let p1, p2 be FinSequence of REAL ; :: 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
A2: len p1 = width m and
A3: for i being Nat st i in Seg (width m) holds
p1 . i = Sum (Col (m,i)) and
A4: len p2 = width m and
A5: for i being Nat st i in Seg (width m) holds
p2 . i = Sum (Col (m,i)) ; :: thesis: p1 = p2
A6: dom p1 = Seg (width m) by A2, 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 A7: j in dom p1 ; :: thesis: p1 . j = p2 . j
then p1 . j = Sum (Col (m,j)) by A3, A6;
hence p1 . j = p2 . j by A5, A6, A7; :: thesis: verum

end;

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