let S be 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)
A1: dom ((len s) (#) (FDprobSEQ s)) = dom (FDprobSEQ s) by VALUED_1:def 5
.= Seg (card S) by Def3
.= dom (freqSEQ s) by Def9 ;

now :: thesis: for m being Nat st m in dom ((len s) (#) (FDprobSEQ s)) holds
((len s) (#) (FDprobSEQ s)) . m = (freqSEQ s) . m

let m be Nat; :: thesis: ( m in dom ((len s) (#) (FDprobSEQ s)) implies ((len s) (#) (FDprobSEQ s)) . m = (freqSEQ s) . m )
assume A2: 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, A2, Def9 ;
:: thesis: verum

end;

hence freqSEQ s = (len s) (#) (FDprobSEQ s) by A1; :: thesis: verum