theorem Th17: :: DIST_1:19

for S being non empty finite set
for s being non empty FinSequence of S holds Sum (FDprobSEQ s) = 1