let n be Element of NAT ; :: thesis: #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL
reconsider m = n + 1 as Nat ;
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 by TAYLOR_1:2;
then A3: #Z (n + 1) is_differentiable_on REAL by A2;
A4: dom (#Z n) = REAL by FUNCT_2:def 1;

A5: now :: thesis: for x being object st x in dom ((#Z (n + 1)) `| REAL) holds
((#Z (n + 1)) `| REAL) . x = (((n + 1) (#) (#Z n)) | REAL) . x

let x be object ; :: 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 ;
((#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 ; :: 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