let n be Nat; :: thesis: for a, r, L being Real
for g being Function of REAL,REAL st ( for x being Real holds g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) )
let a, r, L be Real; :: thesis: for g being Function of REAL,REAL st ( for x being Real holds g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) )
let g be Function of REAL,REAL; :: thesis: ( ( for x being Real holds g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L ) implies for x being Real holds
( g is_differentiable_in x & diff (g,x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) ) )
assume A1: for x being Real holds g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L ; :: thesis: for x being Real holds
( g is_differentiable_in x & diff (g,x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) )
A2: dom g = REAL by FUNCT_2:def 1;
deffunc H₁( Real) -> Element of REAL = In (((($1 - a) |^ (n + 1)) / ((n + 1) !)),REAL);
consider f being Function of REAL,REAL such that
A3: for x being Element of REAL holds f . x = H₁(x) from FUNCT_2:sch 4();
A4: for x being Real holds f . x = ((x - a) |^ (n + 1)) / ((n + 1) !)

proof

let x be Real; :: thesis: f . x = ((x - a) |^ (n + 1)) / ((n + 1) !)
x in REAL by XREAL_0:def 1;
then f . x = H₁(x) by A3;
hence f . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ; :: thesis: verum

end;

A5: dom f = REAL by FUNCT_2:def 1;
A6: dom (((r |^ (n + 1)) * L) (#) f) = dom f by VALUED_1:def 5;

A7: now :: thesis: for x being Element of REAL st x in dom (((r |^ (n + 1)) * L) (#) f) holds
(((r |^ (n + 1)) * L) (#) f) . x = g . x

let x be Element of REAL ; :: thesis: ( x in dom (((r |^ (n + 1)) * L) (#) f) implies (((r |^ (n + 1)) * L) (#) f) . x = g . x )
assume x in dom (((r |^ (n + 1)) * L) (#) f) ; :: thesis: (((r |^ (n + 1)) * L) (#) f) . x = g . x
hence (((r |^ (n + 1)) * L) (#) f) . x = ((r |^ (n + 1)) * L) * (f . x) by VALUED_1:def 5
.= ((r |^ (n + 1)) * L) * (((x - a) |^ (n + 1)) / ((n + 1) !)) by A4
.= ((r |^ (n + 1)) * (((x - a) |^ (n + 1)) / ((n + 1) !))) * L
.= (((r |^ (n + 1)) * ((x - a) |^ (n + 1))) / ((n + 1) !)) * L by XCMPLX_1:74
.= (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L by NEWTON:7
.= g . x by A1 ;
:: thesis: verum

end;

A8: for x being Real holds
( ((r |^ (n + 1)) * L) (#) f is_differentiable_in x & diff ((((r |^ (n + 1)) * L) (#) f),x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) )

proof

let x be Real; :: thesis: ( ((r |^ (n + 1)) * L) (#) f is_differentiable_in x & diff ((((r |^ (n + 1)) * L) (#) f),x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) )
A9: ( f is_differentiable_in x & diff (f,x) = ((x - a) |^ n) / (n !) ) by Th47, A4;
hence ((r |^ (n + 1)) * L) (#) f is_differentiable_in x by FDIFF_1:15; :: thesis: diff ((((r |^ (n + 1)) * L) (#) f),x) = r * ((((r * (x - a)) |^ n) / (n !)) * L)
thus diff ((((r |^ (n + 1)) * L) (#) f),x) = ((r |^ (n + 1)) * L) * (diff (f,x)) by A9, FDIFF_1:15
.= ((r |^ (n + 1)) * (((x - a) |^ n) / (n !))) * L by A9
.= (((r |^ (n + 1)) * ((x - a) |^ n)) / (n !)) * L by XCMPLX_1:74
.= (((r * (r |^ n)) * ((x - a) |^ n)) / (n !)) * L by NEWTON:6
.= ((r * ((r |^ n) * ((x - a) |^ n))) / (n !)) * L
.= ((r * ((r * (x - a)) |^ n)) / (n !)) * L by NEWTON:7
.= (r * (((r * (x - a)) |^ n) / (n !))) * L by XCMPLX_1:74
.= r * ((((r * (x - a)) |^ n) / (n !)) * L) ; :: thesis: verum

end;

((r |^ (n + 1)) * L) (#) f = g by A7, PARTFUN1:5, A2, A5, A6;
hence for x being Real holds
( g is_differentiable_in x & diff (g,x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) ) by A8; :: thesis: verum