let n be Element of NAT ; :: thesis: for A being non empty 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 non empty 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 Element of 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 Element of 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 Th18
.= (#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:9, FUNCT_2:def 1;
then (1 / (n + 1)) (#) (#Z (n + 1)) is_differentiable_on REAL by FDIFF_1:20;
then dom (((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL) = dom (#Z n) by A1, FDIFF_1:def 7;
then A3: ((1 / (n + 1)) (#) (#Z (n + 1))) `| REAL = #Z n by A2, PARTFUN1:5;
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:36 ;
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:9;
then A5: (#Z n) | REAL is continuous by FDIFF_1:25;
then (#Z n) | A is continuous by FCONT_1:16;
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:36 ;
(#Z n) | A is bounded by A1, A5, FCONT_1:16, 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, Th18, 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