let a be Real; :: thesis: for n being Nat
for g being Function of REAL,REAL st ( for x being Real holds g . x = (x - a) |^ (n + 1) ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = (n + 1) * ((x - a) |^ n) )
let n be Nat; :: thesis: for g being Function of REAL,REAL st ( for x being Real holds g . x = (x - a) |^ (n + 1) ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = (n + 1) * ((x - a) |^ n) )
let g be Function of REAL,REAL; :: thesis: ( ( for x being Real holds g . x = (x - a) |^ (n + 1) ) implies for x being Real holds
( g is_differentiable_in x & diff (g,x) = (n + 1) * ((x - a) |^ n) ) )
A1: dom g = REAL by FUNCT_2:def 1;
assume A2: for x being Real holds g . x = (x - a) |^ (n + 1) ; :: thesis: for x being Real holds
( g is_differentiable_in x & diff (g,x) = (n + 1) * ((x - a) |^ n) )
defpred S₁[ set ] means $1 in REAL ;
deffunc H₁( Real) -> Element of REAL = In (($1 - a),REAL);
consider f being PartFunc of REAL,REAL such that
A3: for d being Element of REAL holds
( d in dom f iff S₁[d] ) and
A4: for d being Element of REAL st d in dom f holds
f /. d = H₁(d) from PARTFUN2:sch 2();
for x being object st x in REAL holds
x in dom f by A3;
then REAL c= dom f by TARSKI:def 3;
then A5: dom f = REAL by XBOOLE_0:def 10;
A6: for d being Element of REAL holds f . d = d - a

proof

let d be Element of REAL ; :: thesis: f . d = d - a
f /. d = In ((d - a),REAL) by A4, A5;
hence f . d = d - a by A5, PARTFUN1:def 6; :: thesis: verum

end;

A7: for d being Real holds f . d = d - a

proof

let d be Real; :: thesis: f . d = d - a
d in REAL by XREAL_0:def 1;
hence f . d = d - a by A6; :: thesis: verum

end;

reconsider n1 = n + 1 as Element of NAT by ORDINAL1:def 12;
A8: f is Function of REAL,REAL by A5, FUNCT_2:67;
A9: ( dom (#Z n1) = REAL & rng f c= REAL ) by FUNCT_2:def 1;
then A10: dom ((#Z n1) * f) = dom f by RELAT_1:27;

A11: now :: thesis: for x being Element of REAL st x in dom ((#Z n1) * f) holds
((#Z n1) * f) . x = g . x

let x be Element of REAL ; :: thesis: ( x in dom ((#Z n1) * f) implies ((#Z n1) * f) . x = g . x )
assume x in dom ((#Z n1) * f) ; :: thesis: ((#Z n1) * f) . x = g . x
hence ((#Z n1) * f) . x = ((#Z n1) * f) /. x by PARTFUN1:def 6
.= (#Z n1) /. (f /. x) by A5, A10, PARTFUN2:3
.= (#Z n1) . (f . x) by A5, PARTFUN1:def 6
.= (f . x) #Z n1 by TAYLOR_1:def 1
.= (f . x) |^ (n + 1) by PREPOWER:36
.= (x - a) |^ (n + 1) by A6
.= g . x by A2 ;
:: thesis: verum

end;

reconsider n1 = n + 1, nn = n, n0 = (n + 1) - 1 as Element of NAT by ORDINAL1:def 12;
A12: for x being Real holds
( (#Z n1) * f is_differentiable_in x & diff (((#Z n1) * f),x) = (n + 1) * ((x - a) |^ n) )

proof

let x be Real; :: thesis: ( (#Z n1) * f is_differentiable_in x & diff (((#Z n1) * f),x) = (n + 1) * ((x - a) |^ n) )
A13: ( f is_differentiable_in x & #Z n1 is_differentiable_in f . x ) by A8, Lm8, A7, TAYLOR_1:2;
hence (#Z n1) * f is_differentiable_in x by FDIFF_2:13; :: thesis: diff (((#Z n1) * f),x) = (n + 1) * ((x - a) |^ n)
reconsider pp = (f . x) #Z n0 as Real ;
reconsider px = (x - a) #Z nn as Real ;
diff ((#Z n1),(f . x)) = n1 * pp by TAYLOR_1:2;
hence diff (((#Z n1) * f),x) = (n1 * pp) * (diff (f,x)) by A13, FDIFF_2:13
.= (n1 * pp) * 1 by A8, Lm8, A7
.= n1 * px by A7
.= (n + 1) * ((x - a) |^ n) by PREPOWER:36 ;
:: thesis: verum

end;

(#Z n1) * f = g by A11, PARTFUN1:5, A1, A5, A9, RELAT_1:27;
hence for x being Real holds
( g is_differentiable_in x & diff (g,x) = (n + 1) * ((x - a) |^ n) ) by A12; :: thesis: verum