let x be Element of ExtREAL ; :: thesis: for k being natural number st 0 <= x holds
0 <= x |^ k
let k be natural number ; :: thesis: ( 0 <= x implies 0 <= x |^ k )
assume A1: 0 <= x ; :: thesis: 0 <= x |^ k
defpred S₁[ natural number ] means 0 <= x |^ $1;
A2: S₁[ 0 ] by Th6, FINSEQ_2:72;
A3: for k being natural number st S₁[k] holds
S₁[k + 1]

proof

let k be natural number ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
x |^ (k + 1) = (x |^ k) * x by Th10;
hence S₁[k + 1] by A1, A4; :: thesis: verum

end;

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