theorem Th75: :: NUMPOLY1:75

for n being Nat holds (8 * (Triangle n)) + 1 = ((2 * n) + 1) ^2