let a, b be Nat; :: thesis: for m being non zero Nat holds
( a = 0 iff ((a,b) In_Power m) . 1 = 0 )
for m being non zero Nat st a = 0 holds
((a,b) In_Power m) . 1 = 0
proof
let m be non zero 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
end;
hence for m being non zero Nat holds
( a = 0 iff ((a,b) In_Power m) . 1 = 0 ) by Th45; :: thesis: verum