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:3;
then k in dom (canFS S) by A3, FINSEQ_1:def 3;
then (canFS S) . k is Element of S by A2, FUNCT_1:3;
then consider a being Element of S such that
A4: a = (canFS S) . k ;
set y = (len s) * ((FDprobSEQ s) . k);
take (len s) * ((FDprobSEQ s) . k) ; :: thesis: ( (len s) * ((FDprobSEQ s) . k) is Element of NAT & S₁[k,(len s) * ((FDprobSEQ s) . k)] )
k in dom (FDprobSEQ s) by A3, Def3;
then A6: (len s) * ((FDprobSEQ s) . k) = (len s) * (FDprobability (a,s)) by A4, Def3;
(len s) * ((FDprobSEQ s) . k) is Element of NAT

proof

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

suppose s = {} ; :: thesis: (len s) * ((FDprobSEQ s) . k) is Element of NAT

hence (len s) * ((FDprobSEQ s) . k) is Element of NAT by A6; :: thesis: verum

end;

suppose s <> {} ; :: thesis: (len s) * ((FDprobSEQ s) . k) is Element of NAT

hence (len s) * ((FDprobSEQ s) . k) is Element of NAT by A6, XCMPLX_1:87; :: thesis: verum

end;

end;

end;

hence ( (len s) * ((FDprobSEQ s) . k) is Element of NAT & S₁[k,(len s) * ((FDprobSEQ s) . k)] ) ; :: 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