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))

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 )
;

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;hence frequency (x,s) = (len s) * (FDprobability (x,s)) ; :: thesis: verum