let a1, a2 be Real_Sequence; :: thesis: ( ( 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) ; :: thesis: a1 = a2

now :: thesis: for y being object st y in NAT holds
a1 . y = a2 . y

let y be object ; :: thesis: ( y in NAT implies a1 . y = a2 . y )
assume y in NAT ; :: thesis: a1 . y = a2 . y
then reconsider i = y as Nat ;
thus a1 . y = (((- 1) |^ i) * (r |^ ((2 * i) + 1))) / ((2 * i) + 1) by A3
.= a2 . y by A4 ; :: thesis: verum

end;

hence a1 = a2 ; :: thesis: verum