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

( a = 0 iff ((a,b) In_Power m) . 1 = 0 ) by Th45; :: thesis: verum

( 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

hence
for m being non zero Nat holds
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;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

( a = 0 iff ((a,b) In_Power m) . 1 = 0 ) by Th45; :: thesis: verum