defpred S₁[ Nat, object ] means $2 = (g . $1) * (('F' (f_0 (m,p))) . (In ($1,F_Real)));
A1: for k being Nat st k in Seg m holds
ex x being Element of F_Real st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg m implies ex x being Element of F_Real st S₁[k,x] )
assume k in Seg m ; :: thesis: ex x being Element of F_Real st S₁[k,x]
reconsider r = (g . k) * (('F' (f_0 (m,p))) . (In (k,F_Real))) as Element of F_Real by XREAL_0:def 1;
take r ; :: thesis: S₁[k,r]
thus S₁[k,r] ; :: thesis: verum

end;

consider f being FinSequence of F_Real such that
A2: ( dom f = Seg m & ( for k being Nat st k in Seg m holds
S₁[k,f . k] ) ) from FINSEQ_1:sch 5(A1);
take f ; :: thesis: ( len f = m & ( for i being Nat st i in dom f holds
f . i = (g . i) * (('F' (f_0 (m,p))) . (In (i,F_Real))) ) )
Seg (len f) = Seg m by FINSEQ_1:def 3, A2;
hence ( len f = m & ( for i being Nat st i in dom f holds
f . i = (g . i) * (('F' (f_0 (m,p))) . (In (i,F_Real))) ) ) by A2, FINSEQ_1:6; :: thesis: verum