let X be non empty set ; 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; 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; 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; 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; ( 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
; 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 )
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
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
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
hence
(lim (Partial_Sums G)) | E = (lim (Partial_Sums F)) | E
by A8, A20, A13, A22, PARTFUN1:5;
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
; ( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
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; verum