let n be Element of NAT ; :: thesis:
let A be closed-interval Subset of REAL ; :: thesis:
A1: ( dom (#Z n) = [#] REAL & dom (#Z (n + 1)) = [#] REAL & [#] REAL = dom ((1 / (n + 1)) (#) (#Z (n + 1))) ) by FUNCT_2:def 1;
A2: #Z n is_differentiable_on REAL

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

end;

B1: #Z (n + 1) is_differentiable_on REAL

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:

end;

B2: (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL by A1, B1, FDIFF_1:28;
(#Z n) | REAL is continuous by A2, FDIFF_1:33;
then (#Z n) | A is continuous by FCONT_1:17;
then A3: ( #Z n is_integrable_on A & (#Z n) | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
A4: for x being Real st x in dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) holds
(((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) . x = (#Z n) . x

let x be Real; :: thesis:
assume x in dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) ; :: thesis:
(((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) . x = x #Z n by Th24
.= (#Z n) . x by TAYLOR_1:def 1 ;
hence (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) . x = (#Z n) . x ; :: thesis:

end;

dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) = dom (#Z n) by A1, B2, FDIFF_1:def 8;
then ((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL = #Z n by A4, PARTFUN1:34;
hence integral (#Z n),A = (((1 / (n + 1)) (#) (#Z (n + 1))) . (sup A)) - (((1 / (n + 1)) (#) (#Z (n + 1))) . (inf A)) by A3, Th24, INTEGRA5:13; :: thesis: