let m be non zero Element of NAT ; :: thesis: for a, r, L being Real
for g being Function of REAL,REAL st ( for x being Real holds g . x = r * ((((r * (x - a)) |^ m) / (m !)) * L) ) holds
for x being Real holds g is_differentiable_in x
let a, r, L be Real; :: thesis: for g being Function of REAL,REAL st ( for x being Real holds g . x = r * ((((r * (x - a)) |^ m) / (m !)) * L) ) holds
for x being Real holds g is_differentiable_in x
let g be Function of REAL,REAL; :: thesis: ( ( for x being Real holds g . x = r * ((((r * (x - a)) |^ m) / (m !)) * L) ) implies for x being Real holds g is_differentiable_in x )
assume A1: for x being Real holds g . x = r * ((((r * (x - a)) |^ m) / (m !)) * L) ; :: thesis: for x being Real holds g is_differentiable_in x
A2: dom g = REAL by FUNCT_2:def 1;
reconsider n = m - 1 as Element of NAT by ORDINAL1:def 12;
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();
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 = H₁(x) by A3;
hence f . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ; :: thesis: verum

end;

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

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

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

end;

A7: for x being Real holds ((r |^ (n + 2)) * L) (#) f is_differentiable_in x

proof

let x be Real; :: thesis: ((r |^ (n + 2)) * L) (#) f is_differentiable_in x
f is_differentiable_in x by ORDEQ_01:47, a3;
hence ((r |^ (n + 2)) * L) (#) f is_differentiable_in x by FDIFF_1:15; :: thesis: verum

end;

((r |^ (n + 2)) * L) (#) f = g by A6, A2, A5, PARTFUN1:5;
hence for x being Real holds g is_differentiable_in x by A7; :: thesis: verum