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 ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative ) ; :: thesis: 0 <= integral+ M,f
then consider F1 being Functional_Sequence of X,ExtREAL , K1 being ExtREAL_sequence such that
A1: ( ( for n being Nat holds
( F1 . n is_simple_func_in S & dom (F1 . n) = dom f ) ) & ( for n being Nat holds F1 . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom f holds
( F1 # x is convergent & lim (F1 # x) = f . x ) ) & ( for n being Nat holds K1 . n = integral' M,(F1 . n) ) & K1 is convergent & integral+ M,f = lim K1 ) by Def15;
A2: for n being Nat holds 0 <= K1 . n

proof

let n be Nat; :: thesis: 0 <= K1 . n
( K1 . n = integral' M,(F1 . n) & F1 . n is_simple_func_in S & F1 . n is nonnegative ) by A1;
hence 0 <= K1 . n by Th74; :: thesis: verum

end;

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 )
assume A3: n <= m ; :: thesis: K1 . n <= K1 . m
A4: ( F1 . n is_simple_func_in S & F1 . m is_simple_func_in S & dom (F1 . n) = dom f & dom (F1 . m) = dom f & F1 . n is nonnegative & F1 . m is nonnegative & K1 . m = integral' M,(F1 . m) ) by A1;
A5: 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 A1, A3, A4; :: thesis: verum

end;

then A6: integral' M,((F1 . n) | (dom ((F1 . m) - (F1 . n)))) <= integral' M,((F1 . m) | (dom ((F1 . m) - (F1 . n)))) by A4, Th76;
dom ((F1 . m) - (F1 . n)) = (dom (F1 . m)) /\ (dom (F1 . n)) by A4, A5, Th75;
then ( (F1 . n) | (dom ((F1 . m) - (F1 . n))) = F1 . n & (F1 . m) | (dom ((F1 . m) - (F1 . n))) = F1 . m ) by A4, GRFUNC_1:64;
hence K1 . n <= K1 . m by A1, A4, A6; :: thesis: verum

end;

then lim K1 = sup (rng K1) by Th60;
then K1 . 0 <= lim K1 by Th62;
hence 0 <= integral+ M,f by A1, A2; :: thesis: verum