let a be Complex; :: thesis: for n being natural Number st 0 <> a holds
0 <> a |^ n
let n be natural Number ; :: thesis: ( 0 <> a implies 0 <> a |^ n )
A1: n is Nat by TARSKI:1;
defpred S₁[ Nat] means a |^ $1 <> 0 ;
assume A2: 0 <> a ; :: thesis: 0 <> a |^ n
A3: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume a |^ m <> 0 ; :: thesis: S₁[m + 1]
then (a |^ m) * a <> 0 by A2;
hence S₁[m + 1] by NEWTON:6; :: thesis: verum

end;

A4: S₁[ 0 ] by NEWTON:4;
for m being Nat holds S₁[m] from NAT_1:sch 2(A4, A3);
hence 0 <> a |^ n by A1; :: thesis: verum