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