let A be non empty closed_interval Subset of REAL; :: thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds

f . x >= g . x ) holds

integral f >= integral g

let f, g be Function of A,REAL; :: thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds

f . x >= g . x ) implies integral f >= integral g )

assume that

A1: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable ) and

A2: for x being Real st x in A holds

f . x >= g . x ; :: thesis: integral f >= integral g

A3: dom (f - g) = A by FUNCT_2:def 1;

A4: for x being Real st x in A holds

(f - g) . x >= 0

hence integral f >= integral g by A4, Th32, XREAL_1:49; :: thesis: verum

f . x >= g . x ) holds

integral f >= integral g

let f, g be Function of A,REAL; :: thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds

f . x >= g . x ) implies integral f >= integral g )

assume that

A1: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable ) and

A2: for x being Real st x in A holds

f . x >= g . x ; :: thesis: integral f >= integral g

A3: dom (f - g) = A by FUNCT_2:def 1;

A4: for x being Real st x in A holds

(f - g) . x >= 0

proof

( integral (f - g) = (integral f) - (integral g) & (f - g) | (A /\ A) is bounded )
by A1, Th33, RFUNCT_1:84;
let x be Real; :: thesis: ( x in A implies (f - g) . x >= 0 )

assume A5: x in A ; :: thesis: (f - g) . x >= 0

then (f - g) . x = (f . x) - (g . x) by A3, VALUED_1:13;

hence (f - g) . x >= 0 by A2, A5, XREAL_1:48; :: thesis: verum

end;assume A5: x in A ; :: thesis: (f - g) . x >= 0

then (f - g) . x = (f . x) - (g . x) by A3, VALUED_1:13;

hence (f - g) . x >= 0 by A2, A5, XREAL_1:48; :: thesis: verum

hence integral f >= integral g by A4, Th32, XREAL_1:49; :: thesis: verum