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 ((1 / (n + 1)) (#) (#Z (n + 1))) by FUNCT_2:def 1;
( [#] REAL = dom (#Z (n + 1)) & ( for x being Real st x in REAL holds
#Z (n + 1) is_differentiable_in x ) ) by FUNCT_2:def 1, TAYLOR_1:2;
then A2: #Z (n + 1) is_differentiable_on REAL by FDIFF_1:9;
hence (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL by A1, FDIFF_1:20; :: thesis: for x being Real holds (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n
A3: for x being Real st x in REAL holds
((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n)

proof

set m = n + 1;
let x be Real; :: thesis: ( x in REAL implies ((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n) )
assume A4: x in REAL ; :: thesis: ((#Z (n + 1)) `| REAL) . x = (n + 1) * (x #Z n)
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 7, A4; :: thesis: verum

end;

A5: 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 A6: 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:20, A6
.= (1 / (n + 1)) * (((#Z (n + 1)) `| REAL) . x) by A2, FDIFF_1:def 7, A6
.= (1 / (n + 1)) * ((n + 1) * (x #Z n)) by A3, A6
.= ((1 / (n + 1)) * (n + 1)) * (x #Z n)
.= ((n + 1) / (n + 1)) * (x #Z n) by XCMPLX_1:99
.= 1 * (x #Z n) by XCMPLX_1:60 ;
hence (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n ; :: thesis: verum

end;

let x be Real; :: thesis: (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n
x in REAL by XREAL_0:def 1;
hence (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) . x = x #Z n by A5; :: thesis: verum