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 H1( 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 = H1(x) from a3: 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 = H1(x) by A3;
hence f . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ; :: thesis: verum
end;
A5: dom (((r |^ (n + 1)) * L) (#) f) = REAL by FUNCT_2:def 1;
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 a3
.= (((r |^ (n + 1)) * ((x - a) |^ (n + 1))) / ((n + 1) !)) * L
.= (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L by NEWTON:7
.= g . x by A1 ;
:: thesis: verum
end;
then A6: ((r |^ (n + 1)) * L) (#) f = g by ;
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) )
A8: ( f is_differentiable_in x & diff (f,x) = ((x - a) |^ n) / (n !) ) by ;
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
.= (((r |^ (n + 1)) * ((x - a) |^ n)) / (n !)) * L by A8
.= (((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) ; :: thesis: verum
end;
hence for x being Real holds
( g is_differentiable_in x & diff (g,x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) ) by A6; :: thesis: verum