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

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