defpred S₁[ Nat] means +infty |^ $1 = +infty ;
A1: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
+infty |^ (k + 1) = (+infty |^ k) * +infty by Th10;
hence S₁[k + 1] by A2, XXREAL_3:def 5; :: thesis: verum

end;

A3: S₁[1] by Th9;
for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A3, A1);
hence for k being Nat st 1 <= k holds
+infty |^ k = +infty ; :: thesis: verum