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

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

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

consider K being ExtREAL_sequence such that
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)

lim (F # x) = sup (rng (F # x)) by A12, MESFUNC5:54;

hence g . x <= lim (F # x) by A15, MESFUNC5:56; :: thesis: verum

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

A15:
g . x = (F # x) . 0
by MESFUNC5:def 13;(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;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

lim (F # x) = sup (rng (F # x)) by A12, MESFUNC5:54;

hence g . x <= lim (F # x) by A15, MESFUNC5:56; :: thesis: verum

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

hence
integral+ (M,f) = integral+ ((COM M),f)
by A18, A1, A19, A3, A20, A5, A6, A7, A17, MESFUNC5:def 15; :: thesis: verum
let n be Nat; :: thesis: K . n = integral' ((COM M),(F . n))

A21: K . n = integral' (M,(F . n)) by A16;

end;A21: K . n = integral' (M,(F . n)) by A16;

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

end;

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