let p1, p2 be FinSequence of COMPLEX ; :: thesis: ( len p1 = len z & ( for i being Nat st 1 <= i & i <= len z holds
p1 . i = (z . i) *' ) & len p2 = len z & ( for i being Nat st 1 <= i & i <= len z holds
p2 . i = (z . i) *' ) implies p1 = p2 )
assume that
A5: len p1 = len z and
A6: for i being Nat st 1 <= i & i <= len z holds
(z . i) *' = p1 . i and
A7: len p2 = len z and
A8: for i being Nat st 1 <= i & i <= len z holds
(z . i) *' = p2 . i ; :: thesis: p1 = p2
for i being Nat st 1 <= i & i <= len p1 holds
p1 . i = p2 . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len p1 implies p1 . i = p2 . i )
assume A9: ( 1 <= i & i <= len p1 ) ; :: thesis: p1 . i = p2 . i
then (z . i) *' = p1 . i by A5, A6;
hence p1 . i = p2 . i by A5, A8, A9; :: thesis: verum

end;

hence p1 = p2 by A5, A7, FINSEQ_1:14; :: thesis: verum