defpred S_{1}[ 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_{1}[k,x]

A6: ( dom g = Seg (card S) & ( for n being Nat st n in Seg (card S) holds

S_{1}[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 A6; :: thesis: verum

A1: for k being Nat st k in Seg (card S) holds

ex x being Element of NAT st S

proof

consider g being FinSequence of NAT such that
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_{1}[k,x] )

assume A3: k in Seg (card S) ; :: thesis: ex x being Element of NAT st S_{1}[k,x]

Seg (len (canFS S)) = Seg (card S) by FINSEQ_1:93;

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 ;

reconsider y = (len s) * ((FDprobSEQ s) . k) as Real ;

take y ; :: thesis: ( y is set & y is Element of NAT & S_{1}[k,y] )

k in dom (FDprobSEQ s) by A3, Def3;

then A5: y = (len s) * (FDprobability (a,s)) by A4, Def3;

y is Element of NAT hence ( y is set & y is Element of NAT & S_{1}[k,y] )
; :: thesis: verum

end;let k be Nat; :: thesis: ( k in Seg (card S) implies ex x being Element of NAT st S

assume A3: k in Seg (card S) ; :: thesis: ex x being Element of NAT st S

Seg (len (canFS S)) = Seg (card S) by FINSEQ_1:93;

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 ;

reconsider y = (len s) * ((FDprobSEQ s) . k) as Real ;

take y ; :: thesis: ( y is set & y is Element of NAT & S

k in dom (FDprobSEQ s) by A3, Def3;

then A5: y = (len s) * (FDprobability (a,s)) by A4, Def3;

y is Element of NAT hence ( y is set & y is Element of NAT & S

A6: ( dom g = Seg (card S) & ( for n being Nat st n in Seg (card S) holds

S

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 A6; :: thesis: verum