for S being non empty finite set
for D being Element of distribution_family S
for s being FinSequence of S st s in D holds
D = Finseq-EQclass s