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 by FUNCT_2:def 1;
A2: 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;

( dom (#Z (n + 1)) = [#] REAL & ( for x being Real st x in REAL holds
#Z (n + 1) is_differentiable_in x ) ) by FUNCT_2:def 1, TAYLOR_1:2;
then ( [#] REAL = dom ((1 / (n + 1)) (#) (#Z (n + 1))) & #Z (n + 1) is_differentiable_on REAL ) by FDIFF_1:16, FUNCT_2:def 1;
then (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL by FDIFF_1:28;
then dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL ) = dom (#Z n) by A1, FDIFF_1:def 8;
then A3: ((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL = #Z n by A2, PARTFUN1:34;
A4: (#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 ;
for x being Real st x in REAL holds
#Z n is_differentiable_in x by TAYLOR_1:2;
then #Z n is_differentiable_on REAL by A1, FDIFF_1:16;
then A5: (#Z n) | REAL is continuous by FDIFF_1:33;
then (#Z n) | A is continuous by FCONT_1:17;
then A6: #Z n is_integrable_on A by A1, INTEGRA5:11;
A7: (#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 ;
(#Z n) | A is bounded by A1, A5, FCONT_1:17, INTEGRA5:10;
then integral (#Z n),A = (((1 / (n + 1)) (#) (#Z (n + 1))) . (upper_bound A)) - (((1 / (n + 1)) (#) (#Z (n + 1))) . (lower_bound A)) by A6, 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 A4, A7 ;
hence integral (#Z n),A = ((1 / (n + 1)) * ((upper_bound A) |^ (n + 1))) - ((1 / (n + 1)) * ((lower_bound A) |^ (n + 1))) ; :: thesis: verum