let S be non empty finite set ; :: thesis: for s being FinSequence of S holds freqSEQ s = (len s) * (FDprobSEQ s)
let s be FinSequence of S; :: thesis: freqSEQ s = (len s) * (FDprobSEQ s)
P1: dom ((len s) (#) (FDprobSEQ s)) = dom (FDprobSEQ s) by VALUED_1:def 5
.= Seg (card S) by defFREQDIST
.= dom (freqSEQ s) by defDIST ;

now

let m be Nat; :: thesis: ( m in dom ((len s) (#) (FDprobSEQ s)) implies ((len s) (#) (FDprobSEQ s)) . m = (freqSEQ s) . m )
assume A1: m in dom ((len s) (#) (FDprobSEQ s)) ; :: thesis: ((len s) (#) (FDprobSEQ s)) . m = (freqSEQ s) . m
hence ((len s) (#) (FDprobSEQ s)) . m = (len s) * ((FDprobSEQ s) . m) by VALUED_1:def 5
.= (freqSEQ s) . m by A1, P1, defDIST ;
:: thesis: verum

end;

hence freqSEQ s = (len s) (#) (FDprobSEQ s) by FINSEQ_1:17, P1; :: thesis: verum