defpred S_{1}[ Nat, object ] means $2 = FDprobability (((canFS S) . $1),s);

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

ex x being Element of REAL st S_{1}[k,x]

A3: ( 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 = FDprobability (((canFS S) . n),s) ) )

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

g . n = FDprobability (((canFS S) . n),s) ) ) by A3; :: thesis: verum

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

ex x being Element of REAL st S

proof

consider g being FinSequence of REAL such that
let k be Nat; :: thesis: ( k in Seg (card S) implies ex x being Element of REAL st S_{1}[k,x] )

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

consider x being Real such that

A2: S_{1}[k,x]
;

reconsider x = x as Element of REAL by XREAL_0:def 1;

take x ; :: thesis: S_{1}[k,x]

thus S_{1}[k,x]
by A2; :: thesis: verum

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

consider x being Real such that

A2: S

reconsider x = x as Element of REAL by XREAL_0:def 1;

take x ; :: thesis: S

thus S

A3: ( 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 = FDprobability (((canFS S) . n),s) ) )

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

g . n = FDprobability (((canFS S) . n),s) ) ) by A3; :: thesis: verum