theorem Th24: :: PEPIN:24

for n being Nat holds n |^ 2 = n ^2