let a1, a2 be Real_Sequence; ( ( for n being Nat holds a1 . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) ) & ( for n being Nat holds a2 . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) ) implies a1 = a2 )
assume that
A3:
for i being Nat holds a1 . i = (((- 1) |^ i) * (r |^ ((2 * i) + 1))) / ((2 * i) + 1)
and
A4:
for i being Nat holds a2 . i = (((- 1) |^ i) * (r |^ ((2 * i) + 1))) / ((2 * i) + 1)
; a1 = a2
hence
a1 = a2
; verum