defpred S₁[ Nat, set ] means $2 = (len s) * ((FDprobSEQ s) . $1);
A1: for k being Nat st k in Seg (card S) holds
ex x being Element of NAT st S₁[k,x]

proof

A2: rng (canFS S) = S by FUNCT_2:def 3;
let k be Nat; :: thesis: ( k in Seg (card S) implies ex x being Element of NAT st S₁[k,x] )
assume A3: k in Seg (card S) ; :: thesis: ex x being Element of NAT st S₁[k,x]
Seg (len (canFS S)) = Seg (card S) by UPROOTS:5;
then k in dom (canFS S) by A3, FINSEQ_1:def 3;
then (canFS S) . k is Element of S by A2, FUNCT_1:12;
then consider a being Element of S such that
A4: a = (canFS S) . k ;
consider y being Real such that
A5: y = (len s) * ((FDprobSEQ s) . k) ;
take y ; :: thesis: ( y is Element of NAT & S₁[k,y] )
k in dom (FDprobSEQ s) by A3, Def3;
then A6: y = (len s) * (FDprobability a,s) by A5, A4, Def3;
y is Element of NAT

proof

per cases ( s = {} or s <> {} ) ;

suppose s = {} ; :: thesis: y is Element of NAT

hence y is Element of NAT by A6; :: thesis: verum

end;

suppose s <> {} ; :: thesis: y is Element of NAT

hence y is Element of NAT by A6, XCMPLX_1:88; :: thesis: verum

end;

end;

end;

hence ( y is Element of NAT & S₁[k,y] ) by A5; :: thesis: verum

end;

consider g being FinSequence of NAT such that
A7: ( dom g = Seg (card S) & ( for n being Nat st n in Seg (card S) holds
S₁[n,g . n] ) ) from FINSEQ_1:sch 5(A1);
take g ; :: thesis: ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = (len s) * ((FDprobSEQ s) . n) ) )
thus ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = (len s) * ((FDprobSEQ s) . n) ) ) by A7; :: thesis: verum