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 A1: ( E c= dom f & f is nonnegative & f is_measurable_on E & 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) ) ) ) ; :: thesis:

per cases ;

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, Cor131a; :: thesis:

end;

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

for n being Element of NAT holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) by A1;
then E common_on_dom F by A2, SEQFUNC:def 10;
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, Cor131b; :: thesis:

end;