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 & ( for i being Nat st i in dom p holds
p1 . i = Sum (p | i) ) ) and
A3: ( len p2 = len p & ( 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 ( 1 <= i & i <= len p1 ) ; :: thesis: p1 . i = p2 . i
then A4: i in dom p by A2, FINSEQ_3:27;
then p1 . i = Sum (p | i) by A2;
hence p1 . i = p2 . i by A3, A4; :: thesis: verum

end;

hence p1 = p2 by A2, A3, FINSEQ_1:18; :: thesis: verum