let n be Element of NAT ; :: thesis: #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL
reconsider m = n + 1 as natural number ;
dom (((n + 1) (#) (#Z n)) | REAL) = (dom ((n + 1) (#) (#Z n))) /\ REAL by RELAT_1:61;
then A1: dom (((n + 1) (#) (#Z n)) | REAL) = REAL /\ REAL by FUNCT_2:def 1;
A2: dom (#Z (n + 1)) = REAL by FUNCT_2:def 1;
for x being Real st x in REAL holds
(#Z (n + 1)) | REAL is_differentiable_in x

proof

let x be Real; :: thesis: ( x in REAL implies (#Z (n + 1)) | REAL is_differentiable_in x )
assume x in REAL ; :: thesis: (#Z (n + 1)) | REAL is_differentiable_in x
#Z (n + 1) is_differentiable_in x by TAYLOR_1:2;
hence (#Z (n + 1)) | REAL is_differentiable_in x by A2, RELAT_1:68; :: thesis: verum

end;

then A3: #Z (n + 1) is_differentiable_on REAL by A2, FDIFF_1:def 6;
A4: dom (#Z n) = REAL by FUNCT_2:def 1;

A5: now

let x be set ; :: thesis: ( x in dom ((#Z (n + 1)) `| REAL) implies ((#Z (n + 1)) `| REAL) . x = (((n + 1) (#) (#Z n)) | REAL) . x )
assume A6: x in dom ((#Z (n + 1)) `| REAL) ; :: thesis: ((#Z (n + 1)) `| REAL) . x = (((n + 1) (#) (#Z n)) | REAL) . x
then reconsider z = x as real number ;
((#Z (n + 1)) `| REAL) . x = diff ((#Z (n + 1)),z) by A3, A6, FDIFF_1:def 7;
then ((#Z (n + 1)) `| REAL) . x = m * (z #Z (m - 1)) by TAYLOR_1:2;
then A7: ((#Z (n + 1)) `| REAL) . x = (n + 1) * ((#Z n) . x) by TAYLOR_1:def 1;
x in dom (#Z n) by A4, A6;
then x in dom ((n + 1) (#) (#Z n)) by VALUED_1:def 5;
then ((#Z (n + 1)) `| REAL) . x = ((n + 1) (#) (#Z n)) . x by A7, VALUED_1:def 5;
hence ((#Z (n + 1)) `| REAL) . x = (((n + 1) (#) (#Z n)) | REAL) . x by A1, A6, FUNCT_1:47; :: thesis: verum

end;

dom ((#Z (n + 1)) `| REAL) = REAL by A3, FDIFF_1:def 7;
then (#Z (n + 1)) `| REAL = ((n + 1) (#) (#Z n)) | REAL by A1, A5, FUNCT_1:2;
hence #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL by A3, Lm1; :: thesis: verum