let k be Nat; :: thesis: PrimeDivisors (((2 |^ k) * ((2 |^ k) - 2)) + 1) = PrimeDivisors ((2 |^ k) - 1)
PrimeDivisors (((2 |^ k) * ((2 |^ k) - 2)) + 1) = PrimeDivisors (((2 |^ k) - 1) * ((2 |^ k) - 1))
.= (PrimeDivisors ((2 |^ k) - 1)) \/ (PrimeDivisors ((2 |^ k) - 1)) by DivisorsMulti
.= PrimeDivisors ((2 |^ k) - 1) ;
hence PrimeDivisors (((2 |^ k) * ((2 |^ k) - 2)) + 1) = PrimeDivisors ((2 |^ k) - 1) ; :: thesis: verum