let k be Nat; :: thesis: for x being real number st x > 0 holds
x |^ k > 0
let x be real number ; :: thesis: ( x > 0 implies x |^ k > 0 )
defpred S₁[ Nat] means for x being real number st x > 0 holds
x |^ $1 > 0 ;
A1: S₁[ 0 ] by RVSUM_1:124;
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 A3: for x being real number st x > 0 holds
x |^ k > 0 ; :: thesis: S₁[k + 1]
let x be real number ; :: thesis: ( x > 0 implies x |^ (k + 1) > 0 )
assume x > 0 ; :: thesis: x |^ (k + 1) > 0
then ( x > 0 & x |^ k > 0 & x |^ (k + 1) = x * (x |^ k) ) by A3, Th11;
hence x |^ (k + 1) > 0 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence ( x > 0 implies x |^ k > 0 ) ; :: thesis: verum