per cases ( n is zero or not n is zero ) ;

suppose n is zero ; :: thesis: not a |^ n is light

hence not a |^ n is light by NEWTON:4; :: thesis: verum

end;

suppose not n is zero ; :: thesis: not a |^ n is light

then reconsider n = n as non zero Nat ;
defpred S₁[ Nat] means not a |^ (a + 1) is light ;
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume not a |^ (k + 1) is light ; :: thesis: S₁[k + 1]
then not a * (a |^ (k + 1)) is light ;
hence S₁[k + 1] by NEWTON:6; :: thesis: verum

end;

A3: for l being Nat holds S₁[l] from NAT_1:sch 2(A1, A2);
reconsider m = n - 1 as Nat ;
not a |^ (m + 1) is light by A3;
hence not a |^ n is light ; :: thesis: verum

end;

end;