theorem Th7: :: DIST_2:7

for S being non empty finite set
for D being EqSampleSpaces of S holds (GenProbSEQ S) . D is distProbFinS of S