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:
assume that
A1: E c= dom (F . 0 ) and
B1: F is additive and
B2: F is with_the_same_dom and
A2: for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) and
A3: for x being Element of X st x in E holds
F # x is summable ; :: thesis:
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL :] = (F . $1) | E;
consider G being Functional_Sequence of X,ExtREAL such that
P1: for n being Nat holds G . n = H₁(n) from SEQFUNC:sch 1();
reconsider G = G as with_the_same_dom additive Functional_Sequence of X,ExtREAL by P1, B1, B2, Lm17, Lem09;
dom ((F . 0 ) | E) = E by A1, RELAT_1:91;
then P4: E = dom (G . 0 ) by P1;
P5: for n being Nat holds
( G . n is nonnegative & G . n is_measurable_on E )

let n be Nat; :: thesis:
F . n is nonnegative by A2;
then (F . n) | E is nonnegative by MESFUNC5:21;
hence G . n is nonnegative by P1; :: thesis:
thus G . n is_measurable_on E by P1, A1, B2, A2, Prop1; :: thesis:

end;

for x being Element of X st x in E holds
G # x is summable by A1, P1, A3, Prop2;
then consider I being ExtREAL_sequence such that
P6: ( ( for n being Nat holds I . n = Integral M,((G . n) | E) ) & I is summable & Integral M,((lim (Partial_Sums G)) | E) = Sum I ) by P4, P5, Th131x;
take I ; :: thesis:
R0: for x being Element of X st x in E holds
F # x = G # x

let x be Element of X; :: thesis:
assume R10: x in E ; :: thesis:
for n' being set st n' in NAT holds
(F # x) . n' = (G # x) . n'

let n' be set ; :: thesis:
assume n' in NAT ; :: thesis:
then reconsider n = n' as Nat ;
R11: (F # x) . n = (F . n) . x by MESFUNC5:def 13;
dom (G . n) = E by P4, MESFUNC8:def 2;
then x in dom ((F . n) | E) by P1, R10;
then ((F . n) | E) . x = (F . n) . x by FUNCT_1:70;
then (G . n) . x = (F . n) . x by P1;
hence (F # x) . n' = (G # x) . n' by R11, MESFUNC5:def 13; :: thesis:

end;

hence F # x = G # x by FUNCT_2:18; :: thesis:

end;

P8: (lim (Partial_Sums G)) | E = (lim (Partial_Sums F)) | E

set PG = Partial_Sums G;
set PF = Partial_Sums F;
set E1 = dom (F . 0 );
dom ((Partial_Sums F) . 0 ) = dom (F . 0 ) by ADD0, B1, B2;
then P82: E c= dom (lim (Partial_Sums F)) by A1, MESFUNC8:def 10;
P80: ( dom ((Partial_Sums G) . 0 ) = dom (G . 0 ) & dom ((Partial_Sums F) . 0 ) = dom (F . 0 ) ) by B1, B2, ADD0;
Q1: dom (lim (Partial_Sums G)) = dom ((Partial_Sums G) . 0 ) by MESFUNC8:def 10;
then P84: dom ((lim (Partial_Sums G)) | E) = dom (lim (Partial_Sums G)) by P4, P80, RELAT_1:91;
dom ((lim (Partial_Sums F)) | E) = E by P82, RELAT_1:91;
then P85: dom ((lim (Partial_Sums G)) | E) = dom ((lim (Partial_Sums F)) | E) by P80, Q1, P4, RELAT_1:91;
P86: for x being Element of X st x in dom (lim (Partial_Sums G)) holds
(lim (Partial_Sums G)) . x = (lim (Partial_Sums F)) . x

let x be Element of X; :: thesis:
assume Q01: x in dom (lim (Partial_Sums G)) ; :: thesis:
then Q02: x in E by ADD0, Q1, P4;
set PFx = Partial_Sums (F # x);
set PGx = Partial_Sums (G # x);
for n being Element of NAT holds ((Partial_Sums G) # x) . n = ((Partial_Sums F) # x) . n

let n be Element of NAT ; :: thesis:
( (Partial_Sums (G # x)) . n = ((Partial_Sums G) # x) . n & (Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n ) by A1, B1, B2, P4, Q02, Cor00;
hence ((Partial_Sums G) # x) . n = ((Partial_Sums F) # x) . n by Q02, R0; :: thesis:

end;

then Q05: lim ((Partial_Sums G) # x) = lim ((Partial_Sums F) # x) by FUNCT_2:113;
(lim (Partial_Sums G)) . x = lim ((Partial_Sums G) # x) by Q01, MESFUNC8:def 10;
hence (lim (Partial_Sums G)) . x = (lim (Partial_Sums F)) . x by Q05, Q02, P82, MESFUNC8:def 10; :: thesis:

end;

let x be Element of X; :: thesis:
assume Q07: x in dom ((lim (Partial_Sums G)) | E) ; :: thesis:
then Q09: (lim (Partial_Sums G)) . x = (lim (Partial_Sums F)) . x by P86, P84;
((lim (Partial_Sums F)) | E) . x = (lim (Partial_Sums F)) . x by Q07, P85, FUNCT_1:70;
hence ((lim (Partial_Sums G)) | E) . x = ((lim (Partial_Sums F)) | E) . x by Q09, Q07, FUNCT_1:70; :: thesis:

end;

hence (lim (Partial_Sums G)) | E = (lim (Partial_Sums F)) | E by P85, PARTFUN1:34; :: thesis:

end;

now

let n be Nat; :: thesis:
((F . n) | E) | E = (F . n) | E by RELAT_1:101;
then (G . n) | E = (F . n) | E by P1;
hence I . n = Integral M,((F . n) | E) by P6; :: thesis:

end;

hence ( ( for n being Nat holds I . n = Integral M,((F . n) | E) ) & I is summable & Integral M,((lim (Partial_Sums F)) | E) = Sum I ) by P6, P8; :: thesis: