let S be finite set ; :: thesis: for s being FinSequence of S holds Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s))
let s be FinSequence of S; :: thesis: Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s))
freqSEQ s = (len s) * (FDprobSEQ s) by Th12;
hence Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s)) by RVSUM_1:87; :: thesis: verum