let a, b, c, d, e be Real; :: thesis: for f being PartFunc of REAL,REAL st 0 < e & a <= b & c < d & c in [.a,b.] & d in [.a,b.] & [.a,b.] c= dom f & f | ['a,b'] is continuous & ( for t being Real st t in [.a,b.] holds
0 <= f . t ) & ( for t being Real st t in [.c,d.] holds
e <= f . t ) holds
( 0 < e * (d - c) & e * (d - c) <= integral (f,a,b) )
let f be PartFunc of REAL,REAL; :: thesis: ( 0 < e & a <= b & c < d & c in [.a,b.] & d in [.a,b.] & [.a,b.] c= dom f & f | ['a,b'] is continuous & ( for t being Real st t in [.a,b.] holds
0 <= f . t ) & ( for t being Real st t in [.c,d.] holds
e <= f . t ) implies ( 0 < e * (d - c) & e * (d - c) <= integral (f,a,b) ) )
assume A1: ( 0 < e & a <= b & c < d & c in [.a,b.] & d in [.a,b.] & [.a,b.] c= dom f & f | ['a,b'] is continuous & ( for t being Real st t in [.a,b.] holds
0 <= f . t ) & ( for t being Real st t in [.c,d.] holds
e <= f . t ) ) ; :: thesis: ( 0 < e * (d - c) & e * (d - c) <= integral (f,a,b) )
then A2: ['a,b'] = [.a,b.] by INTEGRA5:def 3;
then A3: ( f | ['a,b'] is bounded & f is_integrable_on ['a,b'] ) by A1, INTEGRA5:10, INTEGRA5:11;
then A4: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A1, A2, INTEGRA6:20;
( a in [.a,b.] & b in [.a,b.] ) by A1;
then A5: integral (f,a,b) = ((integral (f,a,c)) + (integral (f,c,d))) + (integral (f,d,b)) by A1, A2, A3, A4, INTEGRA6:20;
A6: ( a <= c & c <= b ) by A1, XXREAL_1:1;
then A7: ['a,c'] = [.a,c.] by INTEGRA5:def 3;
A8: [.a,c.] c= [.a,b.] by A6, XXREAL_1:34;
then A10: ['a,c'] c= [.a,b.] by A6, INTEGRA5:def 3;
A12: ( a in ['a,c'] & c in ['a,c'] ) by A6, A7;
for t being Real st t in [.a,c.] holds
0 <= f . t by A1, A8;
then A14: 0 <= integral (f,a,c) by A1, A6, A10, A12, Th2;
A15: ( a <= d & d <= b ) by A1, XXREAL_1:1;
then A16: ['d,b'] = [.d,b.] by INTEGRA5:def 3;
A17: [.d,b.] c= [.a,b.] by A15, XXREAL_1:34;
then A19: ['d,b'] c= [.a,b.] by A15, INTEGRA5:def 3;
A21: ( b in ['d,b'] & d in ['d,b'] ) by A15, A16;
for t being Real st t in [.d,b.] holds
0 <= f . t by A1, A17;
then A23: 0 <= integral (f,d,b) by A1, A15, A19, A21, Th2;
0 < d - c by A1, XREAL_1:50;
hence 0 < e * (d - c) by A1; :: thesis: e * (d - c) <= integral (f,a,b)
e * (d - c) <= integral (f,c,d) by A1, Th4;
then 0 + (e * (d - c)) <= ((integral (f,a,c)) + (integral (f,d,b))) + (integral (f,c,d)) by A14, A23, XREAL_1:7;
hence e * (d - c) <= integral (f,a,b) by A5; :: thesis: verum