for S being non empty finite set
for p being distProbFinS of S
for s being FinSequence of S st FDprobSEQ s = p holds
( distribution (p,S) = Finseq-EQclass s & s in distribution (p,S) )