let p1, p2 be FinSequence of COMPLEX ; :: thesis: ( len p1 = width M & ( for j being Nat st j in Seg (width M) holds
p1 . j = Sum (Col (M,j)) ) & len p2 = width M & ( for j being Nat st j in Seg (width M) holds
p2 . j = Sum (Col (M,j)) ) implies p1 = p2 )
assume that
A3: len p1 = width M and
A4: for j being Nat st j in Seg (width M) holds
p1 . j = Sum (Col (M,j)) and
A5: len p2 = width M and
A6: for j being Nat st j in Seg (width M) holds
p2 . j = Sum (Col (M,j)) ; :: thesis: p1 = p2
A7: dom p1 = Seg (width M) by A3, FINSEQ_1:def 3;
for j being Nat st j in dom p1 holds
p1 . j = p2 . j
proof
let j be Nat; :: thesis: ( j in dom p1 implies p1 . j = p2 . j )
assume A8: j in dom p1 ; :: thesis: p1 . j = p2 . j
then p1 . j = Sum (Col (M,j)) by A4, A7;
hence p1 . j = p2 . j by A6, A7, A8; :: thesis: verum
end;
hence p1 = p2 by A3, A5, FINSEQ_2:9; :: thesis: verum