let n be Element of NAT ; :: thesis: #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL
A1: ( dom (#Z (n + 1)) = REAL & dom (#Z n) = 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 A1, RELAT_1:97; :: thesis: verum

end;

then A2: #Z (n + 1) is_differentiable_on REAL by A1, FDIFF_1:def 7;
then A3: dom ((#Z (n + 1)) `| REAL ) = REAL by FDIFF_1:def 8;
dom (((n + 1) (#) (#Z n)) | REAL ) = (dom ((n + 1) (#) (#Z n))) /\ REAL by RELAT_1:90;
then A4: dom (((n + 1) (#) (#Z n)) | REAL ) = REAL /\ REAL by FUNCT_2:def 1;
reconsider m = n + 1 as natural number ;

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 A5: 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 A2, A5, FDIFF_1:def 8;
then ((#Z (n + 1)) `| REAL ) . x = m * (z #Z (m - 1)) by TAYLOR_1:2;
then A6: ((#Z (n + 1)) `| REAL ) . x = (n + 1) * ((#Z n) . x) by TAYLOR_1:def 1;
x in dom (#Z n) by A1, A5;
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 A6, VALUED_1:def 5;
hence ((#Z (n + 1)) `| REAL ) . x = (((n + 1) (#) (#Z n)) | REAL ) . x by A4, A5, FUNCT_1:70; :: thesis: verum

end;

then (#Z (n + 1)) `| REAL = ((n + 1) (#) (#Z n)) | REAL by A3, A4, FUNCT_1:9;
hence #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL by A2, Lm1; :: thesis: verum