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
for E being Element of S st E = dom f & f is E -measurable & f is nonnegative holds
integral+ (M,f) = integral+ ((COM M),f)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is E -measurable & f is nonnegative holds
integral+ (M,f) = integral+ ((COM M),f)
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is E -measurable & f is nonnegative holds
integral+ (M,f) = integral+ ((COM M),f)
let f be PartFunc of X,ExtREAL; :: thesis: for E being Element of S st E = dom f & f is E -measurable & f is nonnegative holds
integral+ (M,f) = integral+ ((COM M),f)
let E be Element of S; :: thesis: ( E = dom f & f is E -measurable & f is nonnegative implies integral+ (M,f) = integral+ ((COM M),f) )
assume that
A1: E = dom f and
A2: f is E -measurable and
A3: f is nonnegative ; :: thesis: integral+ (M,f) = integral+ ((COM M),f)
consider F being Functional_Sequence of X,ExtREAL such that
A4: for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) and
A5: for n being Nat holds F . n is nonnegative and
A6: for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x and
A7: for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) by A1, A2, A3, MESFUNC5:64;
reconsider g = F . 0 as PartFunc of X,ExtREAL ;
A8: g is nonnegative by A5;
A9: dom f = dom g by A4;
A10: for x being Element of X st x in dom g holds
( F # x is convergent & g . x <= lim (F # x) )

proof

let x be Element of X; :: thesis: ( x in dom g implies ( F # x is convergent & g . x <= lim (F # x) ) )
assume A11: x in dom g ; :: thesis: ( F # x is convergent & g . x <= lim (F # x) )
hence F # x is convergent by A7, A9; :: thesis: g . x <= lim (F # x)

A12: now :: thesis: for n, m being Nat st n <= m holds
(F # x) . n <= (F # x) . m

let n, m be Nat; :: thesis: ( n <= m implies (F # x) . n <= (F # x) . m )
assume A13: n <= m ; :: thesis: (F # x) . n <= (F # x) . m
A14: (F # x) . m = (F . m) . x by MESFUNC5:def 13;
(F # x) . n = (F . n) . x by MESFUNC5:def 13;
hence (F # x) . n <= (F # x) . m by A6, A13, A11, A9, A14; :: thesis: verum

end;

A15: g . x = (F # x) . 0 by MESFUNC5:def 13;
lim (F # x) = sup (rng (F # x)) by A12, MESFUNC5:54;
hence g . x <= lim (F # x) by A15, MESFUNC5:56; :: thesis: verum

end;

consider K being ExtREAL_sequence such that
A16: for n being Nat holds K . n = integral' (M,(F . n)) and
A17: K is convergent and
sup (rng K) = lim K and
integral' (M,g) <= lim K by A8, A4, A9, A5, A6, A10, MESFUNC5:75;
A18: integral+ (M,f) = lim K by A1, A2, A3, A4, A5, A6, A7, A16, A17, MESFUNC5:def 15;
reconsider E1 = E as Element of COM (S,M) by Th27;
A19: f is E1 -measurable by A2, Th30;
A20: for n being Nat holds
( F . n is_simple_func_in COM (S,M) & dom (F . n) = dom f ) by A4, Th33;
for n being Nat holds K . n = integral' ((COM M),(F . n))

proof

let n be Nat; :: thesis: K . n = integral' ((COM M),(F . n))
A21: K . n = integral' (M,(F . n)) by A16;

per cases ( dom (F . n) <> {} or dom (F . n) = {} ) ;

suppose A22: dom (F . n) <> {} ; :: thesis: K . n = integral' ((COM M),(F . n))

( F . n is_simple_func_in S & F . n is nonnegative ) by A4, A5;
then integral (M,(F . n)) = integral ((COM M),(F . n)) by Th36;
then K . n = integral ((COM M),(F . n)) by A22, A21, MESFUNC5:def 14;
hence K . n = integral' ((COM M),(F . n)) by A22, MESFUNC5:def 14; :: thesis: verum

end;

suppose A23: dom (F . n) = {} ; :: thesis: K . n = integral' ((COM M),(F . n))

then K . n = 0 by A21, MESFUNC5:def 14;
hence K . n = integral' ((COM M),(F . n)) by A23, MESFUNC5:def 14; :: thesis: verum

end;

end;

end;

hence integral+ (M,f) = integral+ ((COM M),f) by A18, A1, A19, A3, A20, A5, A6, A7, A17, MESFUNC5:def 15; :: thesis: verum