let S be non empty 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 Th14;
hence Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s)) by RVSUM_1:117; :: thesis: verum