let a, b, c, d, e be Real; :: thesis: for f being PartFunc of REAL,REAL st 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 [.c,d.] holds
e <= f . t ) holds
e * (d - c) <= integral (f,c,d)
let f be PartFunc of REAL,REAL; :: thesis: ( 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 [.c,d.] holds
e <= f . t ) implies e * (d - c) <= integral (f,c,d) )
assume A1: ( 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 [.c,d.] holds
e <= f . t ) ) ; :: thesis: e * (d - c) <= integral (f,c,d)
then A2: ['a,b'] = [.a,b.] by INTEGRA5:def 3;
set g = REAL --> e;
A3: ( dom (REAL --> e) = REAL & rng (REAL --> e) = {e} ) by FUNCOP_1:8, FUNCT_2:def 1;
then reconsider g = REAL --> e as PartFunc of REAL,REAL by RELSET_1:4;
g is continuous by A3, FCONT_1:39;
then A5: g | ['a,b'] is continuous ;
for t being Real st t in [.c,d.] holds
g . t <= f . t

proof

let t be Real; :: thesis: ( t in [.c,d.] implies g . t <= f . t )
assume A6: t in [.c,d.] ; :: thesis: g . t <= f . t
then e <= f . t by A1;
hence g . t <= f . t by A6, FUNCOP_1:7; :: thesis: verum

end;

then A7: integral (g,c,d) <= integral (f,c,d) by A1, A3, A5, Th3;
for x being Real st x in ['a,b'] holds
g . x = e by FUNCOP_1:7;
hence e * (d - c) <= integral (f,c,d) by A1, A2, A3, A7, INTEGRA6:27; :: thesis: verum