theorem Th62: :: NEWTON02:62

for n being Nat holds ((2 * n) + 1) |^ 2 = ((4 * n) * (n + 1)) + 1