let Z be open Subset of REAL; :: thesis: for n being non zero Nat
for x being Function of REAL,REAL st x is_differentiable_on Z holds
@ ((@ x) |^ n) is_differentiable_on Z
let n be non zero Nat; :: thesis: for x being Function of REAL,REAL st x is_differentiable_on Z holds
@ ((@ x) |^ n) is_differentiable_on Z
let x be Function of REAL,REAL; :: thesis: ( x is_differentiable_on Z implies @ ((@ x) |^ n) is_differentiable_on Z )
assume A1: x is_differentiable_on Z ; :: thesis: @ ((@ x) |^ n) is_differentiable_on Z
defpred S₁[ Nat] means @ ((@ x) |^ $1) is_differentiable_on Z;
A2: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
@ ((@ x) |^ (n + 1)) = ((@ x) |^ n) * (@ x) by Th20
.= (@ ((@ x) |^ n)) (#) (@ (@ x)) by Th13 ;
hence S₁[n + 1] by A1, A3, FDIFF_2:20; :: thesis: verum

end;

A5: S₁[1] by A1, BINOM:8;
for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A5, A2);
hence @ ((@ x) |^ n) is_differentiable_on Z ; :: thesis: verum