let a, b, m be Nat; :: thesis: ( ((a,b) In_Power m) . 1 = 0 implies m <> 0 )
assume A1: ((a,b) In_Power m) . 1 = 0 ; :: thesis: m <> 0
a |^ 0 = 1 by NEWTON:4;
hence m <> 0 by A1, NEWTON:28; :: thesis: verum