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

proof

let k be Nat; :: thesis: ( k in Seg (card S) implies ex x being Element of NAT st S₁[k,x] )
assume SAS1: k in Seg (card S) ; :: thesis: ex x being Element of NAT st S₁[k,x]
then SAS3P: k in dom (FDprobSEQ s) by defFREQDIST;
consider y being Real such that
SAS4: y = (len s) * ((FDprobSEQ s) . k) ;
Seg (len (canFS S)) = Seg (card S) by UPROOTS:5;
then SAS5: k in dom (canFS S) by SAS1, FINSEQ_1:def 3;
rng (canFS S) = S by FUNCT_2:def 3;
then (canFS S) . k is Element of S by SAS5, FUNCT_1:12;
then consider a being Element of S such that
SAS7: a = (canFS S) . k ;
SAS8: y = (len s) * (FDprobability a,s) by SAS3P, SAS4, SAS7, defFREQDIST;
SAS9: 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 SAS8; :: thesis: verum

end;

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

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

end;

end;

end;

take y ; :: thesis: ( y is Element of NAT & S₁[k,y] )
thus ( y is Element of NAT & S₁[k,y] ) by SAS4, SAS9; :: thesis: verum

end;

consider g being FinSequence of NAT such that
P1: ( 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(P0);
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 P1; :: thesis: verum