let X be non empty set ; :: thesis: 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 st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for F being Functional_Sequence of X,ExtREAL st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
let M be sigma_Measure of S; :: thesis: for E being Element of S
for F being Functional_Sequence of X,ExtREAL st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
let E be Element of S; :: thesis: for F being Functional_Sequence of X,ExtREAL st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
let F be Functional_Sequence of X,ExtREAL; :: thesis: ( E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I ) )
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: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
deffunc H1( 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 = H1(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 )
proof
let n be Nat; :: thesis: ( G . n is nonnegative & G . n is E -measurable )
(F . n) | E is nonnegative by A4, MESFUNC5:15;
hence G . n is nonnegative by A6; :: thesis: G . n is E -measurable
thus G . n is E -measurable by A1, A3, A4, A6, Th20; :: thesis: verum
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
proof
let x be Element of X; :: thesis: ( x in E implies F # x = G # x )
assume A10: x in E ; :: thesis: F # x = G # x
for n9 being object st n9 in NAT holds
(F # x) . n9 = (G # x) . n9
proof
let n9 be object ; :: thesis: ( n9 in NAT implies (F # x) . n9 = (G # x) . n9 )
assume n9 in NAT ; :: thesis: (F # x) . n9 = (G # x) . n9
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: verum
end;
hence F # x = G # x ; :: thesis: verum
end;
A12: (lim (Partial_Sums G)) | E = (lim (Partial_Sums F)) | E
proof
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
proof
let x be Element of X; :: thesis: ( x in dom (lim (Partial_Sums G)) implies (lim (Partial_Sums G)) . x = (lim (Partial_Sums F)) . x )
set PFx = Partial_Sums (F # x);
set PGx = Partial_Sums (G # x);
assume A16: x in dom (lim (Partial_Sums G)) ; :: thesis: (lim (Partial_Sums G)) . x = (lim (Partial_Sums F)) . x
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
proof
let n be Element of NAT ; :: thesis: ((Partial_Sums G) # x) . n = ((Partial_Sums F) # x) . n
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: verum
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: verum
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
proof
let x be Element of X; :: thesis: ( x in dom ((lim (Partial_Sums G)) | E) implies ((lim (Partial_Sums G)) | E) . x = ((lim (Partial_Sums F)) | E) . x )
assume A24: x in dom ((lim (Partial_Sums G)) | E) ; :: thesis: ((lim (Partial_Sums G)) | E) . x = ((lim (Partial_Sums F)) | E) . x
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: verum
end;
hence (lim (Partial_Sums G)) | E = (lim (Partial_Sums F)) | E by A8, A20, A13, A22, PARTFUN1:5; :: thesis: verum
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: ( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
now :: thesis: for n being Nat holds I . n = Integral (M,((F . n) | E))
let n be Nat; :: thesis: I . n = Integral (M,((F . n) | E))
((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: verum
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: verum