let p1, p2 be FinSequence of REAL ; :: thesis: ( len p1 = len p & ( for i being Nat st i in dom p holds
p1 . i = Sum (p | i) ) & len p2 = len p & ( for i being Nat st i in dom p holds
p2 . i = Sum (p | i) ) implies p1 = p2 )
assume that
A2: len p1 = len p and
A3: for i being Nat st i in dom p holds
p1 . i = Sum (p | i) and
A4: len p2 = len p and
A5: for i being Nat st i in dom p holds
p2 . i = Sum (p | i) ; :: thesis: p1 = p2
for i being Nat st 1 <= i & i <= len p1 holds
p1 . i = p2 . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len p1 implies p1 . i = p2 . i )
assume that
A6: 1 <= i and
A7: i <= len p1 ; :: thesis: p1 . i = p2 . i
A8: i in dom p by A2, A6, A7, FINSEQ_3:25;
then p1 . i = Sum (p | i) by A3;
hence p1 . i = p2 . i by A5, A8; :: thesis: verum

end;

hence p1 = p2 by A2, A4, FINSEQ_1:14; :: thesis: verum