let n be Nat; :: thesis:
let r be Real; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
set Z0 = #Z 0;
set Z2 = #Z 2;
set N = 2 * n;
set Zn = #Z (2 * n);
set f = (#Z (2 * n)) / ((#Z 0) + (#Z 2));
assume A1: ( A = [.0,r.] & r >= 0 ) ; :: thesis:
A2: ( (#Z (2 * n)) / ((#Z 0) + (#Z 2)) is continuous & dom ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) = REAL ) by Th4;
then dom (((#Z (2 * n)) / ((#Z 0) + (#Z 2))) | A) = A by RELAT_1:62;
then ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) | A is total by PARTFUN1:def 2;
then reconsider fA = ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) || A as Function of A,REAL ;
A3: ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) | A is continuous by A2;
then A4: ( ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) | A is bounded & (#Z (2 * n)) / ((#Z 0) + (#Z 2)) is_integrable_on A & fA | A = ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) | A ) by INTEGRA5:11, INTEGRA5:10, A2;
A5: fA is integrable by A3, INTEGRA5:def 1, INTEGRA5:11, A2;
A6: ( #Z (2 * n) is continuous & dom (#Z (2 * n)) = REAL ) by FUNCT_2:def 1;
then dom ((#Z (2 * n)) | A) = A by RELAT_1:62;
then (#Z (2 * n)) | A is total by PARTFUN1:def 2;
then reconsider ZnA = (#Z (2 * n)) || A as Function of A,REAL ;
A7: (#Z (2 * n)) | A is continuous ;
then A8: ( (#Z (2 * n)) | A is bounded & #Z (2 * n) is_integrable_on A & ZnA | A = (#Z (2 * n)) | A ) by INTEGRA5:11, INTEGRA5:10, A6;
A9: ZnA is integrable by A7, INTEGRA5:def 1, INTEGRA5:11, A6;
for r being Real st r in A holds
fA . r <= ZnA . r

let r be Real; :: thesis:
assume r in A ; :: thesis:
then A10: ( fA . r = ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) . r & ZnA . r = (#Z (2 * n)) . r ) by FUNCT_1:49;
A11: (#Z (2 * n)) . r = r #Z (2 * n) by TAYLOR_1:def 1
.= r |^ (2 * n) by PREPOWER:36 ;
A12: r |^ (2 * n) >= 0 by POWER:3;
(r ^2) + 1 >= 1 + 0 by XREAL_1:6;
then 1 / (1 + (r ^2)) <= 1 by XREAL_1:183;
then ((r |^ (2 * n)) * 1) / (1 + (r ^2)) <= (r |^ (2 * n)) * 1 by A12, XREAL_1:64;
hence fA . r <= ZnA . r by A11, Th4, A10; :: thesis:

end;

then A13: integral fA <= integral ZnA by A4, A5, A8, A9, INTEGRA2:34;
A14: integral (((#Z (2 * n)) / ((#Z 0) + (#Z 2))),A) = integral fA by INTEGRA5:def 2;
A15: ( lower_bound A = 0 & upper_bound A = r ) by A1, JORDAN5A:19;
A16: 2 * n in NAT by ORDINAL1:def 12;
0 |^ ((2 * n) + 1) = 0 by NEWTON:84;
then A17: (1 / ((2 * n) + 1)) * (0 |^ ((2 * n) + 1)) = 0 ;
A18: integral ZnA = integral ((#Z (2 * n)),A) by INTEGRA5:def 2
.= ((1 / ((2 * n) + 1)) * (r |^ ((2 * n) + 1))) - 0 by A16, A15, A17, INTEGRA9:19 ;
A19: dom (abs ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))) = dom ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) by VALUED_1:def 11;
for x being object st x in REAL holds
((#Z (2 * n)) / ((#Z 0) + (#Z 2))) . x = (abs ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))) . x

let x be object ; :: thesis:
assume x in REAL ; :: thesis:
then reconsider r = x as Element of REAL ;
2 * n = n + n ;
then A20: r |^ (2 * n) = (r |^ n) * (r |^ n) by NEWTON:8;
A21: ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) . r = (r |^ (2 * n)) / (1 + (r ^2)) by Th4;
thus (abs ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))) . x = |.(((#Z (2 * n)) / ((#Z 0) + (#Z 2))) . r).| by A2, A19, VALUED_1:def 11
.= ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) . x by A20, A21, ABSVALUE:def 1 ; :: thesis:

end;

then A22: abs ((#Z (2 * n)) / ((#Z 0) + (#Z 2))) = (#Z (2 * n)) / ((#Z 0) + (#Z 2)) by A19, A2;
|.(integral (((#Z (2 * n)) / ((#Z 0) + (#Z 2))),A)).| <= integral ((abs ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))),A) by A2, INTEGRA6:7, A4;
hence |.(integral (((#Z (2 * n)) / ((#Z 0) + (#Z 2))),A)).| <= (1 / ((2 * n) + 1)) * (r |^ ((2 * n) + 1)) by A13, A14, A18, XXREAL_0:2, A22; :: thesis: