theorem :: NEWTON01:26

for k, m being Nat
for a1, b1 being Complex st (a1 |^ (m + 2)) - (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) + ((a1 * b1) * k)) * (a1 - b1) & a1 * b1 <> 0 holds
(a1 |^ m) - (b1 |^ m) = (a1 - b1) * k