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