defpred S₁[ Nat, object ] means $2 = - ((g . $1) * (((power F_Real) . (z0,$1)) * (('F' (f_0 (m,p))) . 0)));
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]
set r = - ((g . k) * (((power F_Real) . (z0,k)) * (('F' (f_0 (m,p))) . 0)));
reconsider r = - ((g . k) * (((power F_Real) . (z0,k)) * (('F' (f_0 (m,p))) . 0))) 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) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ) )
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) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ) ) by A2, FINSEQ_1:6; :: thesis: verum