theorem :: NUMBER02:43

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