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
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) and
A5: 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
A6: 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 A2, A3, A6, Th18, Th31;
A7: for n being Nat holds
( G . n is nonnegative & G . n is E -measurable )

let n be Nat; :: thesis:
(F . n) | E is nonnegative by A4, MESFUNC5:15;
hence G . n is nonnegative by A6; :: thesis:
thus G . n is E -measurable by A1, A3, A4, A6, Th20; :: thesis:

end;

dom ((F . 0) | E) = E by A1, RELAT_1:62;
then A8: E = dom (G . 0) by A6;
A9: for x being Element of X st x in E holds
F # x = G # x

let x be Element of X; :: thesis:
assume A10: x in E ; :: thesis:
for n9 being object st n9 in NAT holds
(F # x) . n9 = (G # x) . n9

let n9 be object ; :: thesis:
assume n9 in NAT ; :: thesis:
then reconsider n = n9 as Nat ;
dom (G . n) = E by A8, MESFUNC8:def 2;
then x in dom ((F . n) | E) by A6, A10;
then ((F . n) | E) . x = (F . n) . x by FUNCT_1:47;
then A11: (G . n) . x = (F . n) . x by A6;
(F # x) . n = (F . n) . x by MESFUNC5:def 13;
hence (F # x) . n9 = (G # x) . n9 by A11, MESFUNC5:def 13; :: thesis:

end;

hence F # x = G # x ; :: thesis:

end;

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

set E1 = dom (F . 0);
set PF = Partial_Sums F;
set PG = Partial_Sums G;
A13: dom (lim (Partial_Sums G)) = dom ((Partial_Sums G) . 0) by MESFUNC8:def 9;
dom ((Partial_Sums F) . 0) = dom (F . 0) by A2, A3, Th29;
then A14: E c= dom (lim (Partial_Sums F)) by A1, MESFUNC8:def 9;
A15: 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:
set PFx = Partial_Sums (F # x);
set PGx = Partial_Sums (G # x);
assume A16: x in dom (lim (Partial_Sums G)) ; :: thesis:
then A17: x in E by A8, A13, Th29;
for n being Element of NAT holds ((Partial_Sums G) # x) . n = ((Partial_Sums F) # x) . n

let n be Element of NAT ; :: thesis:
A18: (Partial_Sums (G # x)) . n = ((Partial_Sums G) # x) . n by A8, A17, Th32;
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n by A1, A2, A3, A17, Th32;
hence ((Partial_Sums G) # x) . n = ((Partial_Sums F) # x) . n by A9, A17, A18; :: thesis:

end;

then A19: lim ((Partial_Sums G) # x) = lim ((Partial_Sums F) # x) by FUNCT_2:63;
(lim (Partial_Sums G)) . x = lim ((Partial_Sums G) # x) by A16, MESFUNC8:def 9;
hence (lim (Partial_Sums G)) . x = (lim (Partial_Sums F)) . x by A14, A17, A19, MESFUNC8:def 9; :: thesis:

end;

A20: dom ((Partial_Sums G) . 0) = dom (G . 0) by Th29;
then A21: dom ((lim (Partial_Sums G)) | E) = dom (lim (Partial_Sums G)) by A8, A13;
A22: dom ((lim (Partial_Sums F)) | E) = E by A14, RELAT_1:62;
then A23: dom ((lim (Partial_Sums G)) | E) = dom ((lim (Partial_Sums F)) | E) by A8, A20, A13;
for x being Element of X st x in dom ((lim (Partial_Sums G)) | E) holds
((lim (Partial_Sums G)) | E) . x = ((lim (Partial_Sums F)) | E) . x

let x be Element of X; :: thesis:
assume A24: x in dom ((lim (Partial_Sums G)) | E) ; :: thesis:
then A25: ((lim (Partial_Sums F)) | E) . x = (lim (Partial_Sums F)) . x by A23, FUNCT_1:47;
(lim (Partial_Sums G)) . x = (lim (Partial_Sums F)) . x by A21, A15, A24;
hence ((lim (Partial_Sums G)) | E) . x = ((lim (Partial_Sums F)) | E) . x by A24, A25, FUNCT_1:47; :: thesis:

end;

hence (lim (Partial_Sums G)) | E = (lim (Partial_Sums F)) | E by A8, A20, A13, A22, PARTFUN1:5; :: thesis:

end;

for x being Element of X st x in E holds
G # x is summable by A1, A5, A6, Th21;
then consider I being ExtREAL_sequence such that
A26: for n being Nat holds I . n = Integral (M,((G . n) | E)) and
A27: I is summable and
A28: Integral (M,((lim (Partial_Sums G)) | E)) = Sum I by A8, A7, Lm4;
take I ; :: thesis:

let n be Nat; :: thesis:
((F . n) | E) | E = (F . n) | E ;
then (G . n) | E = (F . n) | E by A6;
hence I . n = Integral (M,((F . n) | E)) by A26; :: 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 A27, A28, A12; :: thesis: