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 :: thesis: for i being Nat st i in dom p1 holds
p1 . i = p2 . i

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:9; :: thesis: verum