let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonnegative holds
0 <= integral+ (M,f)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonnegative holds
0 <= integral+ (M,f)
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonnegative holds
0 <= integral+ (M,f)
let f be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonnegative implies 0 <= integral+ (M,f) )
assume that
A1: ex A being Element of S st
( A = dom f & f is A -measurable ) and
A2: f is nonnegative ; :: thesis: 0 <= integral+ (M,f)
consider F1 being Functional_Sequence of X,ExtREAL, K1 being ExtREAL_sequence such that
A3: for n being Nat holds
( F1 . n is_simple_func_in S & dom (F1 . n) = dom f ) and
A4: for n being Nat holds F1 . n is nonnegative and
A5: for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F1 . n) . x <= (F1 . m) . x and
for x being Element of X st x in dom f holds
( F1 # x is convergent & lim (F1 # x) = f . x ) and
A6: for n being Nat holds K1 . n = integral' (M,(F1 . n)) and
K1 is convergent and
A7: integral+ (M,f) = lim K1 by A1, A2, Def15;
for n, m being Nat st n <= m holds
K1 . n <= K1 . m

proof

let n, m be Nat; :: thesis: ( n <= m implies K1 . n <= K1 . m )
A8: F1 . m is_simple_func_in S by A3;
A9: dom (F1 . m) = dom f by A3;
A10: K1 . m = integral' (M,(F1 . m)) by A6;
A11: dom (F1 . n) = dom f by A3;
assume A12: n <= m ; :: thesis: K1 . n <= K1 . m
A13: for x being object st x in dom ((F1 . m) - (F1 . n)) holds
(F1 . n) . x <= (F1 . m) . x

proof

let x be object ; :: thesis: ( x in dom ((F1 . m) - (F1 . n)) implies (F1 . n) . x <= (F1 . m) . x )
assume x in dom ((F1 . m) - (F1 . n)) ; :: thesis: (F1 . n) . x <= (F1 . m) . x
then x in ((dom (F1 . m)) /\ (dom (F1 . n))) \ ((((F1 . m) " {+infty}) /\ ((F1 . n) " {+infty})) \/ (((F1 . m) " {-infty}) /\ ((F1 . n) " {-infty}))) by MESFUNC1:def 4;
then x in (dom (F1 . m)) /\ (dom (F1 . n)) by XBOOLE_0:def 5;
hence (F1 . n) . x <= (F1 . m) . x by A5, A12, A11, A9; :: thesis: verum

end;

A14: F1 . m is nonnegative by A4;
A15: F1 . n is nonnegative by A4;
A16: F1 . n is_simple_func_in S by A3;
then A17: dom ((F1 . m) - (F1 . n)) = (dom (F1 . m)) /\ (dom (F1 . n)) by A8, A15, A14, A13, Th69;
then A18: (F1 . n) | (dom ((F1 . m) - (F1 . n))) = F1 . n by A11, A9, GRFUNC_1:23;
A19: (F1 . m) | (dom ((F1 . m) - (F1 . n))) = F1 . m by A11, A9, A17, GRFUNC_1:23;
integral' (M,((F1 . n) | (dom ((F1 . m) - (F1 . n))))) <= integral' (M,((F1 . m) | (dom ((F1 . m) - (F1 . n))))) by A16, A8, A15, A14, A13, Th70;
hence K1 . n <= K1 . m by A6, A10, A18, A19; :: thesis: verum

end;

then lim K1 = sup (rng K1) by Th54;
then A20: K1 . 0 <= lim K1 by Th56;
for n being Nat holds 0 <= K1 . n

proof

let n be Nat; :: thesis: 0 <= K1 . n
A21: F1 . n is_simple_func_in S by A3;
K1 . n = integral' (M,(F1 . n)) by A6;
hence 0 <= K1 . n by A4, A21, Th68; :: thesis: verum

end;

hence 0 <= integral+ (M,f) by A7, A20; :: thesis: verum