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 & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

f - g is nonnegative

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 & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

f - g is nonnegative

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 & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

f - g is nonnegative

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

g . x <= f . x ) implies f - g is nonnegative )

assume that

A1: f is_simple_func_in S and

A2: g is_simple_func_in S and

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

g . x <= f . x ; :: thesis: f - g is nonnegative

g is () by A2, Th14;

then not -infty in rng g ;

then A4: g " {-infty} = {} by FUNCT_1:72;

f is () by A1, Th14;

then not +infty in rng f ;

then A5: f " {+infty} = {} by FUNCT_1:72;

then ((dom f) /\ (dom g)) \ (((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty}))) = (dom f) /\ (dom g) by A4;

then A6: dom (f - g) = (dom f) /\ (dom g) by MESFUNC1:def 4;

for x being set st x in (dom f) /\ (dom g) holds

( g . x <= f . x & -infty < g . x & f . x < +infty )

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 & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

f - g is nonnegative

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 & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

f - g is nonnegative

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 & ( for x being object st x in dom (f - g) holds

g . x <= f . x ) holds

f - g is nonnegative

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

g . x <= f . x ) implies f - g is nonnegative )

assume that

A1: f is_simple_func_in S and

A2: g is_simple_func_in S and

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

g . x <= f . x ; :: thesis: f - g is nonnegative

g is () by A2, Th14;

then not -infty in rng g ;

then A4: g " {-infty} = {} by FUNCT_1:72;

f is () by A1, Th14;

then not +infty in rng f ;

then A5: f " {+infty} = {} by FUNCT_1:72;

then ((dom f) /\ (dom g)) \ (((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty}))) = (dom f) /\ (dom g) by A4;

then A6: dom (f - g) = (dom f) /\ (dom g) by MESFUNC1:def 4;

for x being set st x in (dom f) /\ (dom g) holds

( g . x <= f . x & -infty < g . x & f . x < +infty )

proof

hence
f - g is nonnegative
by Th21; :: thesis: verum
let x be set ; :: thesis: ( x in (dom f) /\ (dom g) implies ( g . x <= f . x & -infty < g . x & f . x < +infty ) )

assume A7: x in (dom f) /\ (dom g) ; :: thesis: ( g . x <= f . x & -infty < g . x & f . x < +infty )

hence g . x <= f . x by A3, A6; :: thesis: ( -infty < g . x & f . x < +infty )

x in dom g by A7, XBOOLE_0:def 4;

then not g . x in {-infty} by A4, FUNCT_1:def 7;

then not g . x = -infty by TARSKI:def 1;

hence -infty < g . x by XXREAL_0:6; :: thesis: f . x < +infty

x in dom f by A7, XBOOLE_0:def 4;

then not f . x in {+infty} by A5, FUNCT_1:def 7;

then not f . x = +infty by TARSKI:def 1;

hence f . x < +infty by XXREAL_0:4; :: thesis: verum

end;assume A7: x in (dom f) /\ (dom g) ; :: thesis: ( g . x <= f . x & -infty < g . x & f . x < +infty )

hence g . x <= f . x by A3, A6; :: thesis: ( -infty < g . x & f . x < +infty )

x in dom g by A7, XBOOLE_0:def 4;

then not g . x in {-infty} by A4, FUNCT_1:def 7;

then not g . x = -infty by TARSKI:def 1;

hence -infty < g . x by XXREAL_0:6; :: thesis: f . x < +infty

x in dom f by A7, XBOOLE_0:def 4;

then not f . x in {+infty} by A5, FUNCT_1:def 7;

then not f . x = +infty by TARSKI:def 1;

hence f . x < +infty by XXREAL_0:4; :: thesis: verum