let z1, z2 be FinSequence of F_Real; :: thesis: ( len z1 = m & ( for i being Nat st i in dom z1 holds
z1 . i = - ((g . i) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ) & len z2 = m & ( for i being Nat st i in dom z2 holds
z2 . i = - ((g . i) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ) implies z1 = z2 )
assume that
A3: len z1 = m and
A4: for i being Nat st i in dom z1 holds
z1 . i = - ((g . i) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) and
A5: len z2 = m and
A6: for i being Nat st i in dom z2 holds
z2 . i = - ((g . i) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ; :: thesis: z1 = z2
A7: dom z1 = Seg (len z1) by FINSEQ_1:def 3
.= dom z2 by A3, A5, FINSEQ_1:def 3 ;
for x being Nat st x in dom z1 holds
z1 . x = z2 . x

proof

let x be Nat; :: thesis: ( x in dom z1 implies z1 . x = z2 . x )
assume A8: x in dom z1 ; :: thesis: z1 . x = z2 . x
hence z1 . x = - ((g . x) * (((power F_Real) . (z0,x)) * (('F' (f_0 (m,p))) . 0))) by A4
.= z2 . x by A6, A7, A8 ;
:: thesis: verum

end;

hence z1 = z2 by A7; :: thesis: verum