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

then A20: K1 . 0 <= lim K1 by Th56;

for n being Nat holds 0 <= K1 . n

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

then
lim K1 = sup (rng K1)
by Th54;
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

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;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

A14:
F1 . m is nonnegative
by A4;
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;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

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

then A20: K1 . 0 <= lim K1 by Th56;

for n being Nat holds 0 <= K1 . n

proof

hence
0 <= integral+ (M,f)
by A7, A20; :: thesis: verum
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;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