defpred S₁[ 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₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (card S) implies ex x being Element of REAL st S₁[k,x] )
assume k in Seg (card S) ; :: thesis: ex x being Element of REAL st S₁[k,x]
consider x being Real such that
A2: S₁[k,x] ;
reconsider x = x as Element of REAL by XREAL_0:def 1;
take x ; :: thesis: S₁[k,x]
thus S₁[k,x] by A2; :: thesis: verum

end;

consider g being FinSequence of REAL such that
A3: ( 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 = 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