let n be Element of NAT ; :: thesis: ( (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) . x = x #Z n ) )
A1: ( [#] REAL = dom (#Z (n + 1)) & [#] REAL = dom ((1 / (n + 1)) (#) (#Z (n + 1))) ) by FUNCT_2:def 1;
A2: #Z (n + 1) is_differentiable_on REAL

proof

for x being Real st x in REAL holds
#Z (n + 1) is_differentiable_in x by TAYLOR_1:2;
hence #Z (n + 1) is_differentiable_on REAL by A1, FDIFF_1:16; :: thesis: verum

end;

A3: for x being Real st x in REAL holds
((#Z (n + 1)) `| REAL ) . x = (n + 1) * (x #Z n)

proof

let x be Real; :: thesis: ( x in REAL implies ((#Z (n + 1)) `| REAL ) . x = (n + 1) * (x #Z n) )
assume x in REAL ; :: thesis: ((#Z (n + 1)) `| REAL ) . x = (n + 1) * (x #Z n)
set m = n + 1;
diff (#Z (n + 1)),x = (n + 1) * (x #Z ((n + 1) - 1)) by TAYLOR_1:2;
hence ((#Z (n + 1)) `| REAL ) . x = (n + 1) * (x #Z n) by A2, FDIFF_1:def 8; :: thesis: verum

end;

for x being Real st x in REAL holds
(((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) . x = x #Z n

proof

let x be Real; :: thesis: ( x in REAL implies (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) . x = x #Z n )
assume x in REAL ; :: thesis: (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) . x = x #Z n
(((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) . x = (1 / (n + 1)) * (diff (#Z (n + 1)),x) by A1, A2, FDIFF_1:28
.= (1 / (n + 1)) * (((#Z (n + 1)) `| REAL ) . x) by A2, FDIFF_1:def 8
.= (1 / (n + 1)) * ((n + 1) * (x #Z n)) by A3
.= ((1 / (n + 1)) * (n + 1)) * (x #Z n)
.= ((n + 1) / (n + 1)) * (x #Z n) by XCMPLX_1:100
.= 1 * (x #Z n) by XCMPLX_1:60 ;
hence (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) . x = x #Z n ; :: thesis: verum

end;

hence ( (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) . x = x #Z n ) ) by A1, A2, FDIFF_1:28; :: thesis: verum