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_measurable_on A ) & 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_measurable_on A ) & 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_measurable_on A ) & 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_measurable_on A ) & f is nonnegative implies 0 <= integral+ M,f )
assume that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) 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 set st x in dom ((F1 . m) - (F1 . n)) holds
(F1 . n) . x <= (F1 . m) . x

proof

let x be set ; :: 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, Th75;
then A18: (F1 . n) | (dom ((F1 . m) - (F1 . n))) = F1 . n by A11, A9, GRFUNC_1:64;
A19: (F1 . m) | (dom ((F1 . m) - (F1 . n))) = F1 . m by A11, A9, A17, GRFUNC_1:64;
integral' M,((F1 . n) | (dom ((F1 . m) - (F1 . n)))) <= integral' M,((F1 . m) | (dom ((F1 . m) - (F1 . n)))) by A16, A8, A15, A14, A13, Th76;
hence K1 . n <= K1 . m by A6, A10, A18, A19; :: thesis: verum

end;

then lim K1 = sup (rng K1) by Th60;
then A20: K1 . 0 <= lim K1 by Th62;
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, Th74; :: thesis: verum

end;

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