let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) implies integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g)))) )

assume that

A1: f is_simple_func_in S and

A2: g is_simple_func_in S and

A3: f is nonnegative and

A4: g is nonnegative and

A5: for x being object st x in dom (f - g) holds

g . x <= f . x ; :: thesis: integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

(- jj) (#) g is_simple_func_in S by A2, Th39;

then - g is_simple_func_in S by MESFUNC2:9;

then f + (- g) is_simple_func_in S by A1, Th38;

then A6: f - g is_simple_func_in S by MESFUNC2:8;

A7: integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) by A1, A2, A3, A4, A5, Th69;

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & g is_simple_func_in S & f is nonnegative & g is nonnegative & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) implies integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g)))) )

assume that

A1: f is_simple_func_in S and

A2: g is_simple_func_in S and

A3: f is nonnegative and

A4: g is nonnegative and

A5: for x being object st x in dom (f - g) holds

g . x <= f . x ; :: thesis: integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

(- jj) (#) g is_simple_func_in S by A2, Th39;

then - g is_simple_func_in S by MESFUNC2:9;

then f + (- g) is_simple_func_in S by A1, Th38;

then A6: f - g is_simple_func_in S by MESFUNC2:8;

A7: integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) by A1, A2, A3, A4, A5, Th69;

now :: thesis: ( integral' (M,(f | (dom (f - g)))) <> +infty implies integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g)))) )

hence
integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))
by XXREAL_0:4; :: thesis: verumassume
integral' (M,(f | (dom (f - g)))) <> +infty
; :: thesis: integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))

0 <= integral' (M,(f - g)) by A1, A2, A5, A6, Th40, Th68;

hence integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g)))) by A7, XXREAL_3:39; :: thesis: verum

end;0 <= integral' (M,(f - g)) by A1, A2, A5, A6, Th40, Th68;

hence integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g)))) by A7, XXREAL_3:39; :: thesis: verum