let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let E be Element of S; :: thesis:
let F be Functional_Sequence of X,ExtREAL; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
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) ) ; :: thesis:

suppose E = {} ; :: thesis:

hence 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 ) by A1, A3, A5, Lm2; :: thesis:

end;

suppose A7: E <> {} ; :: thesis:

for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) by A5;
then E common_on_dom F by A7, SEQFUNC:def 9;
hence 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 ) by A1, A2, A3, A4, A5, A6, Lm3; :: thesis:

end;

end;