defpred S₁[ Nat] means 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 a |^ (k + 1) is light ; :: thesis: S₁[k + 1]
then 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 ;
a |^ (m + 1) is light by A3;
hence a |^ n is light ; :: thesis: verum