theorem Th10: :: DIST_1:12

for S being finite set
for s being FinSequence of S holds (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s