let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL st 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 ) & ex t0 being Real st
( t0 in ].a,b.[ & 0 < f . t0 ) holds
ex d, c, e being Real st
( 0 < e & c < d & c in [.a,b.] & d in [.a,b.] & 0 < e * (d - c) & e * (d - c) <= integral (f,a,b) )
let f be PartFunc of REAL,REAL; :: thesis: ( 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 ) & ex t0 being Real st
( t0 in ].a,b.[ & 0 < f . t0 ) implies ex d, c, e being Real st
( 0 < e & c < d & c in [.a,b.] & d in [.a,b.] & 0 < e * (d - c) & e * (d - c) <= integral (f,a,b) ) )
assume A1: ( 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 ) & ex t0 being Real st
( t0 in ].a,b.[ & 0 < f . t0 ) ) ; :: thesis: ex d, c, e being Real st
( 0 < e & c < d & c in [.a,b.] & d in [.a,b.] & 0 < e * (d - c) & e * (d - c) <= integral (f,a,b) )
then consider t0 being Real such that
A2: ( t0 in ].a,b.[ & 0 < f . t0 ) ;
A3: ].a,b.[ c= [.a,b.] by Lm1;
set e = (f . t0) / 2;
A4: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then consider s0 being Real such that
A6: ( 0 < s0 & ( for t being Real st t in ['a,b'] & |.(t - t0).| < s0 holds
|.((f . t) - (f . t0)).| < (f . t0) / 2 ) ) by A1, A2, A3, FCONT_1:14;
set s = s0 / 2;
A7: ( 0 < s0 / 2 & s0 / 2 < s0 ) by A6, XREAL_1:216;
reconsider s2 = min ((t0 - a),(b - t0)) as Real ;
A10: ( s2 <= t0 - a & s2 <= b - t0 ) by XXREAL_0:17;
A8: ( a < t0 & t0 < b ) by A2, XXREAL_1:4;
then ( 0 < t0 - a & 0 < b - t0 ) by XREAL_1:50;
then A11: 0 < s2 by XXREAL_0:15;
reconsider s3 = min ((s0 / 2),s2) as Real ;
A12: ( s3 <= s0 / 2 & s3 <= s2 ) by XXREAL_0:17;
A13: 0 < s3 by A6, A11, XXREAL_0:15;
set c = t0 - s3;
set d = t0 + s3;
set e0 = (f . t0) / 2;
take t0 + s3 ; :: thesis: ex c, e being Real st
( 0 < e & c < t0 + s3 & c in [.a,b.] & t0 + s3 in [.a,b.] & 0 < e * ((t0 + s3) - c) & e * ((t0 + s3) - c) <= integral (f,a,b) )
take t0 - s3 ; :: thesis: ex e being Real st
( 0 < e & t0 - s3 < t0 + s3 & t0 - s3 in [.a,b.] & t0 + s3 in [.a,b.] & 0 < e * ((t0 + s3) - (t0 - s3)) & e * ((t0 + s3) - (t0 - s3)) <= integral (f,a,b) )
take (f . t0) / 2 ; :: thesis: ( 0 < (f . t0) / 2 & t0 - s3 < t0 + s3 & t0 - s3 in [.a,b.] & t0 + s3 in [.a,b.] & 0 < ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) & ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) <= integral (f,a,b) )
thus 0 < (f . t0) / 2 by A2; :: thesis: ( t0 - s3 < t0 + s3 & t0 - s3 in [.a,b.] & t0 + s3 in [.a,b.] & 0 < ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) & ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) <= integral (f,a,b) )
A15: t0 - s3 < t0 - 0 by XREAL_1:15, A13;
thus A16: t0 - s3 < t0 + s3 by A13, XREAL_1:8; :: thesis: ( t0 - s3 in [.a,b.] & t0 + s3 in [.a,b.] & 0 < ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) & ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) <= integral (f,a,b) )
A18: t0 - s2 <= t0 - s3 by A12, XREAL_1:13;
s2 + a <= (t0 - a) + a by A10, XREAL_1:7;
then (s2 + a) - s2 <= t0 - s2 by XREAL_1:13;
then A19: ( a <= t0 - s3 & t0 - s3 <= b ) by A8, A15, A18, XXREAL_0:2;
hence A20: t0 - s3 in [.a,b.] ; :: thesis: ( t0 + s3 in [.a,b.] & 0 < ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) & ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) <= integral (f,a,b) )
A21: a + 0 < t0 + s3 by A8, A13, XREAL_1:8;
A22: t0 + s3 <= t0 + s2 by A12, XREAL_1:7;
s2 + t0 <= (b - t0) + t0 by A10, XREAL_1:7;
then A23: ( a <= t0 + s3 & t0 + s3 <= b ) by A21, A22, XXREAL_0:2;
hence A24: t0 + s3 in [.a,b.] ; :: thesis: ( 0 < ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) & ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) <= integral (f,a,b) )
A25: [.(t0 - s3),(t0 + s3).] c= [.a,b.] by A19, A23, XXREAL_1:34;
for t being Real st t in [.(t0 - s3),(t0 + s3).] holds
(f . t0) / 2 <= f . t

proof

let t be Real; :: thesis: ( t in [.(t0 - s3),(t0 + s3).] implies (f . t0) / 2 <= f . t )
assume A27: t in [.(t0 - s3),(t0 + s3).] ; :: thesis: (f . t0) / 2 <= f . t
then ( t0 - s3 <= t & t <= t0 + s3 ) by XXREAL_1:1;
then ( (t0 - s3) - t0 <= t - t0 & t - t0 <= (t0 + s3) - t0 ) by XREAL_1:13;
then |.(t - t0).| <= s3 by ABSVALUE:5;
then |.(t - t0).| <= s0 / 2 by A12, XXREAL_0:2;
then |.(t - t0).| < s0 by A7, XXREAL_0:2;
then |.((f . t) - (f . t0)).| < (f . t0) / 2 by A4, A6, A25, A27;
then ( - ((f . t0) / 2) <= (f . t) - (f . t0) & (f . t) - (f . t0) <= (f . t0) / 2 ) by ABSVALUE:5;
then (- ((f . t0) / 2)) + (f . t0) <= ((f . t) - (f . t0)) + (f . t0) by XREAL_1:7;
hence (f . t0) / 2 <= f . t ; :: thesis: verum

end;

hence ( 0 < ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) & ((f . t0) / 2) * ((t0 + s3) - (t0 - s3)) <= integral (f,a,b) ) by A1, A2, A16, A20, A24, Th5; :: thesis: verum