defpred S_{1}[ set ] means $1 in REAL ;

let n be Nat; :: thesis: 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; :: thesis: 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 H_{1}( 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 S_{1}[d] )
and

A2: for d being Element of REAL st d in dom g holds

g /. d = H_{1}(d)
from PARTFUN2:sch 2();

take g ; :: thesis: ( 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) !)

( (#Z (n + 1)) * f is_differentiable_in x & diff (((#Z (n + 1)) * f),x) = - ((n + 1) * ((b - x) #Z n)) )

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; :: thesis: verum

let n be Nat; :: thesis: 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; :: thesis: 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 H

consider g being PartFunc of REAL,REAL such that

A1: for d being Element of REAL holds

( d in dom g iff S

A2: for d being Element of REAL st d in dom g holds

g /. d = H

take g ; :: thesis: ( 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) !)

proof

let d be Real; :: thesis: g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !)

reconsider d = d as Element of REAL by XREAL_0:def 1;

g /. d = H_{1}(d)
by A2, A8;

hence g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !) by A8, PARTFUN1:def 6; :: thesis: verum

end;reconsider d = d as Element of REAL by XREAL_0:def 1;

g /. d = H

hence g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !) by A8, PARTFUN1:def 6; :: thesis: verum

A10: now :: thesis: for x being Element of REAL st x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) holds

((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x

A11:
for x being Real holds ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x

let x be Element of REAL ; :: thesis: ( x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) implies ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x )

assume x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) ; :: thesis: ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x

hence ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = (l / ((n + 1) !)) * (((#Z (n + 1)) * f) . x) by VALUED_1:def 5

.= (l / ((n + 1) !)) * (((#Z (n + 1)) * f) /. x) by A3, A6, PARTFUN1:def 6

.= (l / ((n + 1) !)) * ((#Z (n + 1)) /. (f /. x)) by A3, A6, PARTFUN2:3

.= (l / ((n + 1) !)) * ((#Z (n + 1)) . (f . x)) by A3, PARTFUN1:def 6

.= (l / ((n + 1) !)) * ((f . x) #Z (n + 1)) by Def1

.= (l / ((n + 1) !)) * ((f . x) |^ (n + 1)) by PREPOWER:36

.= (l / ((n + 1) !)) * ((b - x) |^ (n + 1)) by A4

.= (l * ((b - x) |^ (n + 1))) / ((n + 1) !) by XCMPLX_1:74

.= g . x by A9 ;

:: thesis: verum

end;assume x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) ; :: thesis: ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x

hence ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = (l / ((n + 1) !)) * (((#Z (n + 1)) * f) . x) by VALUED_1:def 5

.= (l / ((n + 1) !)) * (((#Z (n + 1)) * f) /. x) by A3, A6, PARTFUN1:def 6

.= (l / ((n + 1) !)) * ((#Z (n + 1)) /. (f /. x)) by A3, A6, PARTFUN2:3

.= (l / ((n + 1) !)) * ((#Z (n + 1)) . (f . x)) by A3, PARTFUN1:def 6

.= (l / ((n + 1) !)) * ((f . x) #Z (n + 1)) by Def1

.= (l / ((n + 1) !)) * ((f . x) |^ (n + 1)) by PREPOWER:36

.= (l / ((n + 1) !)) * ((b - x) |^ (n + 1)) by A4

.= (l * ((b - x) |^ (n + 1))) / ((n + 1) !) by XCMPLX_1:74

.= g . x by A9 ;

:: thesis: verum

( (#Z (n + 1)) * f is_differentiable_in x & diff (((#Z (n + 1)) * f),x) = - ((n + 1) * ((b - x) #Z n)) )

proof

let xx be Real; :: thesis: ( (#Z (n + 1)) * f is_differentiable_in xx & diff (((#Z (n + 1)) * f),xx) = - ((n + 1) * ((b - xx) #Z n)) )

reconsider x = xx as Real ;

A12: ( f is_differentiable_in x & #Z (n + 1) is_differentiable_in f . x ) by A5, Th2;

hence (#Z (n + 1)) * f is_differentiable_in xx by FDIFF_2:13; :: thesis: diff (((#Z (n + 1)) * f),xx) = - ((n + 1) * ((b - xx) #Z n))

diff ((#Z (n + 1)),(f . x)) = (n + 1) * ((f . x) #Z ((n + 1) - 1)) by Th2;

hence diff (((#Z (n + 1)) * f),xx) = ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (diff (f,x)) by A12, FDIFF_2:13

.= ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (- 1) by A5

.= ((n + 1) * ((b - x) #Z ((n + 1) - 1))) * (- 1) by A4

.= - ((n + 1) * ((b - xx) #Z n)) ;

:: thesis: verum

end;reconsider x = xx as Real ;

A12: ( f is_differentiable_in x & #Z (n + 1) is_differentiable_in f . x ) by A5, Th2;

hence (#Z (n + 1)) * f is_differentiable_in xx by FDIFF_2:13; :: thesis: diff (((#Z (n + 1)) * f),xx) = - ((n + 1) * ((b - xx) #Z n))

diff ((#Z (n + 1)),(f . x)) = (n + 1) * ((f . x) #Z ((n + 1) - 1)) by Th2;

hence diff (((#Z (n + 1)) * f),xx) = ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (diff (f,x)) by A12, FDIFF_2:13

.= ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (- 1) by A5

.= ((n + 1) * ((b - x) #Z ((n + 1) - 1))) * (- 1) by A4

.= - ((n + 1) * ((b - xx) #Z n)) ;

:: thesis: verum

A13: now :: thesis: for x being Real holds

( (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x & diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !)) )

dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) = dom g
by A8, A3, A6, VALUED_1:def 5;( (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x & diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !)) )

let x be Real; :: thesis: ( (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x & diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !)) )

A14: (n + 1) / ((n + 1) !) = (1 * (n + 1)) / ((n !) * (n + 1)) by NEWTON:15

.= 1 / (n !) by XCMPLX_1:91 ;

A15: (#Z (n + 1)) * f is_differentiable_in x by A11;

hence (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x by FDIFF_1:15; :: thesis: diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !))

thus diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = (l / ((n + 1) !)) * (diff (((#Z (n + 1)) * f),x)) by A15, FDIFF_1:15

.= ((diff (((#Z (n + 1)) * f),x)) / ((n + 1) !)) * l by XCMPLX_1:75

.= l * ((- ((n + 1) * ((b - x) #Z n))) / ((n + 1) !)) by A11

.= l * ((- ((n + 1) * ((b - x) |^ n))) / ((n + 1) !)) by PREPOWER:36

.= (l * (- ((n + 1) * ((b - x) |^ n)))) / ((n + 1) !) by XCMPLX_1:74

.= ((- l) * ((n + 1) * ((b - x) |^ n))) / ((n + 1) !)

.= (- l) * (((n + 1) * ((b - x) |^ n)) / ((n + 1) !)) by XCMPLX_1:74

.= (- l) * (((b - x) |^ n) * ((n + 1) / ((n + 1) !))) by XCMPLX_1:74

.= (- l) * (((b - x) |^ n) / (n !)) by A14, XCMPLX_1:99

.= - (l * (((b - x) |^ n) / (n !)))

.= - ((l * ((b - x) |^ n)) / (n !)) by XCMPLX_1:74 ; :: thesis: verum

end;A14: (n + 1) / ((n + 1) !) = (1 * (n + 1)) / ((n !) * (n + 1)) by NEWTON:15

.= 1 / (n !) by XCMPLX_1:91 ;

A15: (#Z (n + 1)) * f is_differentiable_in x by A11;

hence (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x by FDIFF_1:15; :: thesis: diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !))

thus diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = (l / ((n + 1) !)) * (diff (((#Z (n + 1)) * f),x)) by A15, FDIFF_1:15

.= ((diff (((#Z (n + 1)) * f),x)) / ((n + 1) !)) * l by XCMPLX_1:75

.= l * ((- ((n + 1) * ((b - x) #Z n))) / ((n + 1) !)) by A11

.= l * ((- ((n + 1) * ((b - x) |^ n))) / ((n + 1) !)) by PREPOWER:36

.= (l * (- ((n + 1) * ((b - x) |^ n)))) / ((n + 1) !) by XCMPLX_1:74

.= ((- l) * ((n + 1) * ((b - x) |^ n))) / ((n + 1) !)

.= (- l) * (((n + 1) * ((b - x) |^ n)) / ((n + 1) !)) by XCMPLX_1:74

.= (- l) * (((b - x) |^ n) * ((n + 1) / ((n + 1) !))) by XCMPLX_1:74

.= (- l) * (((b - x) |^ n) / (n !)) by A14, XCMPLX_1:99

.= - (l * (((b - x) |^ n) / (n !)))

.= - ((l * ((b - x) |^ n)) / (n !)) by XCMPLX_1:74 ; :: thesis: verum

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; :: thesis: verum