theorem Th12: :: DIST_1:14
for S being finite set
for s being FinSequence of S holds freqSEQ s = (len s) * (FDprobSEQ s)