A0: n is Nat by TARSKI:1;
defpred S₁[ Nat] means x |^ x is natural ;
A1: for a being Nat st S₁[a] holds
S₁[a + 1]

proof

let a be Nat; :: thesis: ( S₁[a] implies S₁[a + 1] )
assume S₁[a] ; :: thesis: S₁[a + 1]
then reconsider b = x |^ a as Nat ;
x |^ (a + 1) = b * x by Th6;
hence S₁[a + 1] ; :: thesis: verum

end;

A2: S₁[ 0 ] by RVSUM_1:94;
for a being Nat holds S₁[a] from NAT_1:sch 2(A2, A1);
hence x |^ n is natural by A0; :: thesis: verum