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 )

proof

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;

hence f - g is nonnegative by Th21; :: thesis: verum