let a be real number ; :: thesis: for n being natural number st 0 < a holds
0 < a |^ n
let n be natural number ; :: thesis: ( 0 < a implies 0 < a |^ n )
defpred S₁[ natural number ] means 0 < a |^ $1;
assume A1: 0 < a ; :: thesis: 0 < a |^ n
A2: S₁[ 0 ] by NEWTON:9;
A3: for m being natural number st S₁[m] holds
S₁[m + 1]

proof

let m be natural number ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume a |^ m > 0 ; :: thesis: S₁[m + 1]
then (a |^ m) * a > 0 * a by A1, XREAL_1:70;
hence S₁[m + 1] by NEWTON:11; :: thesis: verum

end;

for m being natural number holds S₁[m] from NAT_1:sch 2(A2, A3);
hence 0 < a |^ n ; :: thesis: verum