let a, t be Real; :: thesis: for f, g being PartFunc of REAL,REAL st a <= t & ['a,t'] c= dom f & f is_integrable_on ['a,t'] & f | ['a,t'] is bounded & ['a,t'] c= dom g & g is_integrable_on ['a,t'] & g | ['a,t'] is bounded & ( for x being Real st x in ['a,t'] holds
f . x <= g . x ) holds
integral (f,a,t) <= integral (g,a,t)
let f, g be PartFunc of REAL,REAL; :: thesis: ( a <= t & ['a,t'] c= dom f & f is_integrable_on ['a,t'] & f | ['a,t'] is bounded & ['a,t'] c= dom g & g is_integrable_on ['a,t'] & g | ['a,t'] is bounded & ( for x being Real st x in ['a,t'] holds
f . x <= g . x ) implies integral (f,a,t) <= integral (g,a,t) )
assume A1: ( a <= t & ['a,t'] c= dom f & f is_integrable_on ['a,t'] & f | ['a,t'] is bounded & ['a,t'] c= dom g & g is_integrable_on ['a,t'] & g | ['a,t'] is bounded & ( for x being Real st x in ['a,t'] holds
f . x <= g . x ) ) ; :: thesis: integral (f,a,t) <= integral (g,a,t)
set f0 = f | ['a,t'];
set g0 = g | ['a,t'];
A2: dom (f | ['a,t']) = ['a,t'] by A1, RELAT_1:62;
rng (f | ['a,t']) c= REAL ;
then reconsider f0 = f | ['a,t'] as Function of ['a,t'],REAL by A2, FUNCT_2:2;
A3: dom (g | ['a,t']) = ['a,t'] by A1, RELAT_1:62;
rng (g | ['a,t']) c= REAL ;
then reconsider g0 = g | ['a,t'] as Function of ['a,t'],REAL by A3, FUNCT_2:2;
A4: f0 | ['a,t'] is bounded by A1;
A5: f0 is integrable by A1;
A6: g0 | ['a,t'] is bounded by A1;
A7: g0 is integrable by A1;

now :: thesis: for x being Real st x in ['a,t'] holds
f0 . x <= g0 . x

let x be Real; :: thesis: ( x in ['a,t'] implies f0 . x <= g0 . x )
assume A8: x in ['a,t'] ; :: thesis: f0 . x <= g0 . x
A9: f0 . x = f . x by A8, FUNCT_1:49;
g0 . x = g . x by A8, FUNCT_1:49;
hence f0 . x <= g0 . x by A9, A1, A8; :: thesis: verum

end;

then A10: integral (f,['a,t']) <= integral (g,['a,t']) by A4, A5, A6, A7, INTEGRA2:34;
integral (f,['a,t']) = integral (f,a,t) by A1, INTEGRA5:def 4;
hence integral (f,a,t) <= integral (g,a,t) by A10, A1, INTEGRA5:def 4; :: thesis: verum