let n be Nat; 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; 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; ( ( 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
; 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 FUNCT_2:sch 4();
a3:
for x being Real holds f . x = ((x - a) |^ (n + 1)) / ((n + 1) !)
A5:
dom (((r |^ (n + 1)) * L) (#) f) = REAL
by FUNCT_2:def 1;
then A6:
((r |^ (n + 1)) * L) (#) f = g
by PARTFUN1:5, A2, A5;
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) )
hence
for x being Real holds
( g is_differentiable_in x & diff (g,x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) )
by A6; verum