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 S1[ Nat] means FPower (r,$1) is differentiable Function of REAL,REAL;
A1: S1[ 0 ]
proof
FPower (r,0) = the carrier of F_Real --> r by POLYNOM5:66;
hence S1[ 0 ] ; :: thesis: verum
end;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
FPower (r,(n + 1)) = (FPower (r,n)) (#) (id REAL) by Th41;
hence ( S1[n] implies S1[n + 1] ) ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A1, A2);
 hence FPower (r,n) is differentiable Function of REAL,REAL ; :: thesis: verum