let n be Nat; :: thesis: for r being Element of F_Real holds FPower (r,n) is differentiable Function of REAL,REAL
let r be Element of F_Real; :: thesis: FPower (r,n) is differentiable Function of REAL,REAL
defpred S₁[ Nat] means FPower (r,$1) is differentiable Function of REAL,REAL;
A1: S₁[ 0 ]

proof

FPower (r,0) = the carrier of F_Real --> r by POLYNOM5:66;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
FPower (r,(n + 1)) = (FPower (r,n)) (#) (id REAL) by Th41;
hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence FPower (r,n) is differentiable Function of REAL,REAL ; :: thesis: verum