defpred S₁[ Nat, set ] 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] ;
consider g being FinSequence of REAL such that
A2: ( 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 A2; :: thesis: verum