let g be PartFunc of REAL,REAL; :: thesis: for G being Real_Sequence st g is continuous & dom g = ].0,PI.[ & ( for n being Nat holds
( G . n = integral (g,(1 / (n + 1)),(PI - (1 / (n + 1)))) & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom g & g | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & g | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & g is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) ) ) & ( for t being Real st t in ].0,PI.[ holds
0 <= g . t ) holds
for n, m being Nat st n <= m holds
G . n <= G . m
let G be Real_Sequence; :: thesis: ( g is continuous & dom g = ].0,PI.[ & ( for n being Nat holds
( G . n = integral (g,(1 / (n + 1)),(PI - (1 / (n + 1)))) & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom g & g | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & g | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & g is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) ) ) & ( for t being Real st t in ].0,PI.[ holds
0 <= g . t ) implies for n, m being Nat st n <= m holds
G . n <= G . m )
assume A1: ( g is continuous & dom g = ].0,PI.[ & ( for n being Nat holds
( G . n = integral (g,(1 / (n + 1)),(PI - (1 / (n + 1)))) & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom g & g | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & g | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & g is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) ) ) & ( for t being Real st t in ].0,PI.[ holds
0 <= g . t ) ) ; :: thesis: for n, m being Nat st n <= m holds
G . n <= G . m
let n, m be Nat; :: thesis: ( n <= m implies G . n <= G . m )
assume n <= m ; :: thesis: G . n <= G . m
then n + 1 <= m + 1 by XREAL_1:7;
then A2: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
then A3: PI - (1 / (n + 1)) <= PI - (1 / (m + 1)) by XREAL_1:13;
A4: 1 / (n + 1) < PI - (1 / (n + 1)) by Lm3;
A5: 1 / (m + 1) < PI - (1 / (n + 1)) by A2, Lm3, XXREAL_0:2;
A6: 1 / (m + 1) < PI - (1 / (m + 1)) by Lm3;
A7: ( ['(1 / (m + 1)),(PI - (1 / (m + 1)))'] c= dom g & g | ['(1 / (m + 1)),(PI - (1 / (m + 1)))'] is continuous & g | ['(1 / (m + 1)),(PI - (1 / (m + 1)))'] is bounded & g is_integrable_on ['(1 / (m + 1)),(PI - (1 / (m + 1)))'] ) by A1;
A8: ['(1 / (m + 1)),(PI - (1 / (m + 1)))'] = [.(1 / (m + 1)),(PI - (1 / (m + 1))).] by Lm3;
then PI - (1 / (n + 1)) in ['(1 / (m + 1)),(PI - (1 / (m + 1)))'] by A3, A5;
then A10: ( g is_integrable_on ['(1 / (m + 1)),(PI - (1 / (n + 1)))'] & g is_integrable_on ['(PI - (1 / (n + 1))),(PI - (1 / (m + 1)))'] & integral (g,(1 / (m + 1)),(PI - (1 / (m + 1)))) = (integral (g,(1 / (m + 1)),(PI - (1 / (n + 1))))) + (integral (g,(PI - (1 / (n + 1))),(PI - (1 / (m + 1))))) ) by A6, A7, INTEGRA6:17;
A12: ['(1 / (m + 1)),(PI - (1 / (n + 1)))'] c= dom g

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in ['(1 / (m + 1)),(PI - (1 / (n + 1)))'] or t in dom g )
assume A11: t in ['(1 / (m + 1)),(PI - (1 / (n + 1)))'] ; :: thesis: t in dom g
then reconsider s = t as Real ;
s in [.(1 / (m + 1)),(PI - (1 / (n + 1))).] by A11, A5, INTEGRA5:def 3;
then ( 1 / (m + 1) <= s & s <= PI - (1 / (n + 1)) ) by XXREAL_1:1;
then ( 1 / (m + 1) <= s & s <= PI - (1 / (m + 1)) ) by A3, XXREAL_0:2;
then s in ['(1 / (m + 1)),(PI - (1 / (m + 1)))'] by A8;
hence t in dom g by A7; :: thesis: verum

end;

g | ['(1 / (m + 1)),(PI - (1 / (n + 1)))'] is continuous by A1;
then A13: ( g | ['(1 / (m + 1)),(PI - (1 / (n + 1)))'] is bounded & g is_integrable_on ['(1 / (m + 1)),(PI - (1 / (n + 1)))'] ) by A12, INTEGRA5:10, INTEGRA5:11;
['(1 / (m + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (m + 1)),(PI - (1 / (n + 1))).] by A5, INTEGRA5:def 3;
then 1 / (n + 1) in ['(1 / (m + 1)),(PI - (1 / (n + 1)))'] by A2, A4;
then A14: integral (g,(1 / (m + 1)),(PI - (1 / (m + 1)))) = ((integral (g,(1 / (m + 1)),(1 / (n + 1)))) + (integral (g,(1 / (n + 1)),(PI - (1 / (n + 1)))))) + (integral (g,(PI - (1 / (n + 1))),(PI - (1 / (m + 1))))) by A5, A10, A12, A13, INTEGRA6:17;
A15: 1 / (m + 1) in [.(1 / (m + 1)),(PI - (1 / (m + 1))).] by A6;
A16: 1 / (n + 1) <= PI - (1 / (m + 1)) by A3, Lm3, XXREAL_0:2;
then A17: 1 / (n + 1) in [.(1 / (m + 1)),(PI - (1 / (m + 1))).] by A2;
for t being Real st t in [.(1 / (m + 1)),(1 / (n + 1)).] holds
0 <= g . t

proof

let t be Real; :: thesis: ( t in [.(1 / (m + 1)),(1 / (n + 1)).] implies 0 <= g . t )
assume t in [.(1 / (m + 1)),(1 / (n + 1)).] ; :: thesis: 0 <= g . t
then ( 1 / (m + 1) <= t & t <= 1 / (n + 1) ) by XXREAL_1:1;
then ( 1 / (m + 1) <= t & t <= PI - (1 / (m + 1)) ) by A16, XXREAL_0:2;
then A18: t in [.(1 / (m + 1)),(PI - (1 / (m + 1))).] ;
[.(1 / (m + 1)),(PI - (1 / (m + 1))).] c= ].0,PI.[ by Lm3;
hence 0 <= g . t by A1, A18; :: thesis: verum

end;

then A19: 0 <= integral (g,(1 / (m + 1)),(1 / (n + 1))) by A2, A6, A7, A8, A15, A17, Th2;
A20: PI - (1 / (n + 1)) in [.(1 / (m + 1)),(PI - (1 / (m + 1))).] by A3, A5;
A21: PI - (1 / (m + 1)) in [.(1 / (m + 1)),(PI - (1 / (m + 1))).] by A6;
for t being Real st t in [.(PI - (1 / (n + 1))),(PI - (1 / (m + 1))).] holds
0 <= g . t

proof

let t be Real; :: thesis: ( t in [.(PI - (1 / (n + 1))),(PI - (1 / (m + 1))).] implies 0 <= g . t )
assume t in [.(PI - (1 / (n + 1))),(PI - (1 / (m + 1))).] ; :: thesis: 0 <= g . t
then ( PI - (1 / (n + 1)) <= t & t <= PI - (1 / (m + 1)) ) by XXREAL_1:1;
then ( 1 / (m + 1) <= t & t <= PI - (1 / (m + 1)) ) by A5, XXREAL_0:2;
then A22: t in [.(1 / (m + 1)),(PI - (1 / (m + 1))).] ;
[.(1 / (m + 1)),(PI - (1 / (m + 1))).] c= ].0,PI.[ by Lm3;
hence 0 <= g . t by A1, A22; :: thesis: verum

end;

then 0 <= integral (g,(PI - (1 / (n + 1))),(PI - (1 / (m + 1)))) by A3, A6, A7, A8, A20, A21, Th2;
then A23: 0 + (integral (g,(1 / (n + 1)),(PI - (1 / (n + 1))))) <= ((integral (g,(1 / (m + 1)),(1 / (n + 1)))) + (integral (g,(PI - (1 / (n + 1))),(PI - (1 / (m + 1)))))) + (integral (g,(1 / (n + 1)),(PI - (1 / (n + 1))))) by A19, XREAL_1:7;
( G . n = integral (g,(1 / (n + 1)),(PI - (1 / (n + 1)))) & G . m = integral (g,(1 / (m + 1)),(PI - (1 / (m + 1)))) ) by A1;
hence G . n <= G . m by A14, A23; :: thesis: verum