let m be non zero Element of NAT ; 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; 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; ( ( 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)
; for x being Real holds g is_differentiable_in x
A2:
dom g = REAL
by FUNCT_2:def 1;
1 <= m
by NAT_1:14;
then reconsider n = m - 1 as Nat by INT_1:5, ORDINAL1:def 12;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
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 FUNCT_2:sch 4();
A4:
for x being Real holds f . x = ((x - a) |^ (n + 1)) / ((n + 1) !)
A5:
dom f = REAL
by FUNCT_2:def 1;
A6:
dom (((r |^ (n + 2)) * L) (#) f) = dom f
by VALUED_1:def 5;
A8:
for x being Real holds ((r |^ (n + 2)) * L) (#) f is_differentiable_in x
((r |^ (n + 2)) * L) (#) f = g
by A7, A2, A5, A6, PARTFUN1:5;
hence
for x being Real holds g is_differentiable_in x
by A8; verum