let S be finite set ; :: thesis: for s being FinSequence of S
for x being set holds frequency (x,s) = (len s) * (FDprobability (x,s))
let s be FinSequence of S; :: thesis: for x being set holds frequency (x,s) = (len s) * (FDprobability (x,s))
let x be set ; :: thesis: frequency (x,s) = (len s) * (FDprobability (x,s))

per cases ( not s is empty or s is empty ) ;

suppose not s is empty ; :: thesis: frequency (x,s) = (len s) * (FDprobability (x,s))

hence frequency (x,s) = (len s) * (FDprobability (x,s)) by XCMPLX_1:87; :: thesis: verum

end;

suppose s is empty ; :: thesis: frequency (x,s) = (len s) * (FDprobability (x,s))

then frequency (x,s) = 0 ;
hence frequency (x,s) = (len s) * (FDprobability (x,s)) ; :: thesis: verum

end;

end;