theorem Th42: :: NUMBER02:42

for n being Nat holds n ^2 divides ((n + 1) |^ n) - 1