theorem Th13: :: DIST_1:15

for S being finite set
for s being FinSequence of S holds Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s))