let n be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL holds integral (#Z n),A = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1)))
let A be closed-interval Subset of REAL ; :: thesis: integral (#Z n),A = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1)))
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

proof

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: verum

end;

B1: #Z (n + 1) is_differentiable_on REAL

proof

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: verum

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

proof

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

end;

X2: (#Z (n + 1)) . (upper_bound A) = (upper_bound A) #Z (n + 1) by TAYLOR_1:def 1
.= (upper_bound A) |^ (n + 1) by PREPOWER:46 ;
X1: (#Z (n + 1)) . (lower_bound A) = (lower_bound A) #Z (n + 1) by TAYLOR_1:def 1
.= (lower_bound A) |^ (n + 1) by PREPOWER:46 ;
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;
then integral (#Z n),A = (((1 / (n + 1)) (#) (#Z (n + 1))) . (upper_bound A)) - (((1 / (n + 1)) (#) (#Z (n + 1))) . (lower_bound A)) by A3, Th24, INTEGRA5:13
.= ((1 / (n + 1)) * ((#Z (n + 1)) . (upper_bound A))) - (((1 / (n + 1)) (#) (#Z (n + 1))) . (lower_bound A)) by VALUED_1:6
.= ((1 / (n + 1)) * ((#Z (n + 1)) . (upper_bound A))) - ((1 / (n + 1)) * ((#Z (n + 1)) . (lower_bound A))) by VALUED_1:6
.= ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1))) by X1, X2 ;
hence integral (#Z n),A = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1))) ; :: thesis: verum