let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is E -measurable & F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
let S be SigmaField of X; for M being sigma_Measure of S
for E being Element of S
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is E -measurable & F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
let M be sigma_Measure of S; for E being Element of S
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is E -measurable & F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
let E be Element of S; for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is E -measurable & F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
let F be Functional_Sequence of X,ExtREAL; for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is E -measurable & F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
let f be PartFunc of X,ExtREAL; ( E c= dom f & f is nonnegative & f is E -measurable & F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
assume that
A1:
E c= dom f
and
A2:
f is nonnegative
and
A3:
f is E -measurable
and
A4:
F is additive
and
A5:
for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) )
and
A6:
for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) )
; ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )