theorem P136c: :: NUMBER12:54

for k being Nat holds PrimeDivisors (((2 |^ k) * ((2 |^ k) - 2)) + 1) = PrimeDivisors ((2 |^ k) - 1)