defpred S1[ Nat, set ] means \$2 = (len s) * (() . \$1);
A1: for k being Nat st k in Seg (card S) holds
ex x being Element of NAT st S1[k,x]
proof
A2: rng () = S by FUNCT_2:def 3;
let k be Nat; :: thesis: ( k in Seg (card S) implies ex x being Element of NAT st S1[k,x] )
assume A3: k in Seg (card S) ; :: thesis: ex x being Element of NAT st S1[k,x]
Seg (len ()) = Seg (card S) by FINSEQ_1:93;
then k in dom () by ;
then (canFS S) . k is Element of S by ;
then consider a being Element of S such that
A4: a = () . k ;
reconsider y = (len s) * (() . k) as Real ;
take y ; :: thesis: ( y is set & y is Element of NAT & S1[k,y] )
k in dom () by ;
then A5: y = (len s) * (FDprobability (a,s)) by ;
y is Element of NAT
proof end;
hence ( y is set & y is Element of NAT & S1[k,y] ) ; :: thesis: verum
end;
consider g being FinSequence of NAT such that
A6: ( dom g = Seg (card S) & ( for n being Nat st n in Seg (card S) holds
S1[n,g . n] ) ) from take g ; :: thesis: ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = (len s) * (() . n) ) )

thus ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = (len s) * (() . n) ) ) by A6; :: thesis: verum