let p1, p2 be FinSequence of COMPLEX ; :: thesis: ( len p1 = len M & ( for i being Nat st i in Seg (len M) holds
p1 . i = Sum (mlt (Line M,i),F) ) & len p2 = len M & ( for i being Nat st i in Seg (len M) holds
p2 . i = Sum (mlt (Line M,i),F) ) implies p1 = p2 )
assume that
A3: ( len p1 = len M & ( for i being Nat st i in Seg (len M) holds
p1 . i = Sum (mlt (Line M,i),F) ) ) and
A4: ( len p2 = len M & ( for i being Nat st i in Seg (len M) holds
p2 . i = Sum (mlt (Line M,i),F) ) ) ; :: thesis: p1 = p2
X: dom p1 = Seg (len M) by A3, FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom p1 implies p1 . i = p2 . i )
assume A5: i in dom p1 ; :: thesis: p1 . i = p2 . i
then p1 . i = Sum (mlt (Line M,i),F) by A3, X;
hence p1 . i = p2 . i by A4, A5, X; :: thesis: verum

end;

hence p1 = p2 by A3, A4, FINSEQ_2:10; :: thesis: verum