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 S1[ Nat] means not a |^ (a + 1) is light ;
A1: S1[ 0 ] ;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume not a |^ (k + 1) is light ; :: thesis: S1[k + 1]
then not a * (a |^ (k + 1)) is light ;
hence S1[k + 1] by NEWTON:6; :: thesis: verum
end;
A3: for l being Nat holds S1[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;