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
A2: len p1 = len M and
A3: 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 and
A5: for i being Nat st i in Seg (len M) holds
p2 . i = Sum (mlt (Line M,i),F) ; :: thesis: p1 = p2
A6: dom p1 = Seg (len M) by A2, FINSEQ_1:def 3;

now

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

end;

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