defpred S1[ set ] means $1 in REAL ;
let n be Nat; for l, b being Real ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) ) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) )
let l, b be Real; ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) ) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) )
deffunc H1( Real) -> Element of REAL = In (((l * ((b - $1) |^ (n + 1))) / ((n + 1) !)),REAL);
consider g being PartFunc of REAL,REAL such that
A1:
for d being Element of REAL holds
( d in dom g iff S1[d] )
and
A2:
for d being Element of REAL st d in dom g holds
g /. d = H1(d)
from PARTFUN2:sch 2();
take
g
; ( dom g = [#] REAL & ( for x being Real holds g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) ) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) )
consider f being PartFunc of REAL,REAL such that
A3:
dom f = [#] REAL
and
A4:
for x being Real holds f . x = b - x
and
A5:
for x being Real holds
( f is_differentiable_in x & diff (f,x) = - 1 )
by Lm5;
( dom (#Z (n + 1)) = REAL & rng f c= REAL )
by FUNCT_2:def 1;
then A6:
dom ((#Z (n + 1)) * f) = dom f
by RELAT_1:27;
for x being object st x in REAL holds
x in dom g
by A1;
then A7:
REAL c= dom g
by TARSKI:def 3;
then A8:
dom g = [#] REAL
by XBOOLE_0:def 10;
A9:
for d being Real holds g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !)
A11:
for x being Real holds
( (#Z (n + 1)) * f is_differentiable_in x & diff (((#Z (n + 1)) * f),x) = - ((n + 1) * ((b - x) #Z n)) )
dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) = dom g
by A8, A3, A6, VALUED_1:def 5;
then
(l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) = g
by A10, PARTFUN1:5;
hence
( dom g = [#] REAL & ( for x being Real holds g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) ) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) )
by A7, A9, A13, XBOOLE_0:def 10; verum