theorem :: NEWTON02:145

for a, b, m being Nat st ((a,b) In_Power m) . 1 = 0 holds
m <> 0