let S be non empty 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:88; :: thesis: verum

end;

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

then event_pick x,s = {} by RELAT_1:172;
then frequency x,s = 0 ;
hence frequency x,s = (len s) * (FDprobability x,s) ; :: thesis: verum

end;

end;