let n be Element of 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 ! )) ) ) ) ) )
defpred S₁[ set ] means $1 in REAL ;
deffunc H₁( Real) -> Element of REAL = (l * ((b - $1) |^ (n + 1))) / ((n + 1) ! );
consider g being PartFunc of REAL ,REAL such that
A1: for d being Element of REAL holds
( d in dom g iff S₁[d] ) and
A2: for d being Element of REAL st d in dom g holds
g /. d = H₁(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 ! )) ) ) ) ) )
A3: dom g = [#] REAL

proof

for x being set st x in REAL holds
x in dom g by A1;
then REAL c= dom g by TARSKI:def 3;
hence dom g = [#] REAL by XBOOLE_0:def 10; :: thesis: verum

end;

A4: for d being Element of REAL holds g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) ! )

proof

let d be Element of REAL ; :: thesis: g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) ! )
g /. d = (l * ((b - d) |^ (n + 1))) / ((n + 1) ! ) by A2, A3;
hence g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) ! ) by A3, PARTFUN1:def 8; :: thesis: verum

end;

consider f being PartFunc of REAL ,REAL such that
A5: dom f = [#] REAL and
A6: for x being Real holds f . x = b - x and
A7: for x being Real holds
( f is_differentiable_in x & diff f,x = - 1 ) by Lm5;
A8: 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)) )

proof

let x be Real; :: thesis: ( (#Z (n + 1)) * f is_differentiable_in x & diff ((#Z (n + 1)) * f),x = - ((n + 1) * ((b - x) #Z n)) )
A9: f is_differentiable_in x by A7;
A10: ( #Z (n + 1) is_differentiable_in f . x & diff (#Z (n + 1)),(f . x) = (n + 1) * ((f . x) #Z ((n + 1) - 1)) ) by Th2;
hence (#Z (n + 1)) * f is_differentiable_in x by A9, FDIFF_2:13; :: thesis: diff ((#Z (n + 1)) * f),x = - ((n + 1) * ((b - x) #Z n))
thus diff ((#Z (n + 1)) * f),x = ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (diff f,x) by A9, A10, FDIFF_2:13
.= ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (- 1) by A7
.= ((n + 1) * ((b - x) #Z ((n + 1) - 1))) * (- 1) by A6
.= - ((n + 1) * ((b - x) #Z n)) ; :: thesis: verum

end;

A11: (l / ((n + 1) ! )) (#) ((#Z (n + 1)) * f) = g

proof

A12: dom (#Z (n + 1)) = REAL by FUNCT_2:def 1;
rng f c= REAL ;
then A13: dom ((#Z (n + 1)) * f) = dom f by A12, RELAT_1:46;
then A14: dom ((l / ((n + 1) ! )) (#) ((#Z (n + 1)) * f)) = dom g by A3, A5, VALUED_1:def 5;

now

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 A15: x in dom ((l / ((n + 1) ! )) (#) ((#Z (n + 1)) * f)) ; :: thesis: ((l / ((n + 1) ! )) (#) ((#Z (n + 1)) * f)) . x = g . x
thus ((l / ((n + 1) ! )) (#) ((#Z (n + 1)) * f)) . x = (l / ((n + 1) ! )) * (((#Z (n + 1)) * f) . x) by A15, VALUED_1:def 5
.= (l / ((n + 1) ! )) * (((#Z (n + 1)) * f) /. x) by A5, A13, PARTFUN1:def 8
.= (l / ((n + 1) ! )) * ((#Z (n + 1)) /. (f /. x)) by A5, A13, PARTFUN2:6
.= (l / ((n + 1) ! )) * ((#Z (n + 1)) . (f . x)) by A5, PARTFUN1:def 8
.= (l / ((n + 1) ! )) * ((f . x) #Z (n + 1)) by Def1
.= (l / ((n + 1) ! )) * ((f . x) |^ (n + 1)) by PREPOWER:46
.= (l / ((n + 1) ! )) * ((b - x) |^ (n + 1)) by A6
.= (l * ((b - x) |^ (n + 1))) / ((n + 1) ! ) by XCMPLX_1:75
.= g . x by A4 ; :: thesis: verum

end;

hence (l / ((n + 1) ! )) (#) ((#Z (n + 1)) * f) = g by A14, PARTFUN1:34; :: thesis: verum

end;

now

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 ! )) )
A16: (#Z (n + 1)) * f is_differentiable_in x by A8;
hence (l / ((n + 1) ! )) (#) ((#Z (n + 1)) * f) is_differentiable_in x by FDIFF_1:23; :: thesis: diff ((l / ((n + 1) ! )) (#) ((#Z (n + 1)) * f)),x = - ((l * ((b - x) |^ n)) / (n ! ))
A17: (n + 1) / ((n + 1) ! ) = (1 * (n + 1)) / ((n ! ) * (n + 1)) by NEWTON:21
.= 1 / (n ! ) by XCMPLX_1:92 ;
thus diff ((l / ((n + 1) ! )) (#) ((#Z (n + 1)) * f)),x = (l / ((n + 1) ! )) * (diff ((#Z (n + 1)) * f),x) by A16, FDIFF_1:23
.= ((diff ((#Z (n + 1)) * f),x) / ((n + 1) ! )) * l by XCMPLX_1:76
.= l * ((- ((n + 1) * ((b - x) #Z n))) / ((n + 1) ! )) by A8
.= l * ((- ((n + 1) * ((b - x) |^ n))) / ((n + 1) ! )) by PREPOWER:46
.= (l * (- ((n + 1) * ((b - x) |^ n)))) / ((n + 1) ! ) by XCMPLX_1:75
.= ((- l) * ((n + 1) * ((b - x) |^ n))) / ((n + 1) ! )
.= (- l) * (((n + 1) * ((b - x) |^ n)) / ((n + 1) ! )) by XCMPLX_1:75
.= (- l) * (((b - x) |^ n) * ((n + 1) / ((n + 1) ! ))) by XCMPLX_1:75
.= (- l) * (((b - x) |^ n) / (n ! )) by A17, XCMPLX_1:100
.= - (l * (((b - x) |^ n) / (n ! )))
.= - ((l * ((b - x) |^ n)) / (n ! )) by XCMPLX_1:75 ; :: thesis: verum

end;

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 A3, A4, A11; :: thesis: verum