let F1, F2 be Real_Sequence; :: thesis: ( ( for i being Nat holds F1 . i = Sum (S . i) ) & ( for i being Nat holds F2 . i = Sum (S . i) ) implies F1 = F2 )

assume that

A2: for i being Nat holds F1 . i = Sum (S . i) and

A3: for i being Nat holds F2 . i = Sum (S . i) ; :: thesis: F1 = F2

for i being Element of NAT holds F1 . i = F2 . i

assume that

A2: for i being Nat holds F1 . i = Sum (S . i) and

A3: for i being Nat holds F2 . i = Sum (S . i) ; :: thesis: F1 = F2

for i being Element of NAT holds F1 . i = F2 . i

proof

hence
F1 = F2
; :: thesis: verum
let i be Element of NAT ; :: thesis: F1 . i = F2 . i

F1 . i = Sum (S . i) by A2

.= F2 . i by A3 ;

hence F1 . i = F2 . i ; :: thesis: verum

end;F1 . i = Sum (S . i) by A2

.= F2 . i by A3 ;

hence F1 . i = F2 . i ; :: thesis: verum