let X be non empty set ; for S being SigmaField of X
for F, G being Functional_Sequence of X,ExtREAL
for E being Element of S st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | E ) holds
lim (Partial_Sums G) = (lim (Partial_Sums F)) | E
let S be SigmaField of X; for F, G being Functional_Sequence of X,ExtREAL
for E being Element of S st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | E ) holds
lim (Partial_Sums G) = (lim (Partial_Sums F)) | E
let F, G be Functional_Sequence of X,ExtREAL; for E being Element of S st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | E ) holds
lim (Partial_Sums G) = (lim (Partial_Sums F)) | E
let E be Element of S; ( E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | E ) implies lim (Partial_Sums G) = (lim (Partial_Sums F)) | E )
assume that
A1:
E c= dom (F . 0)
and
A2:
F is additive
and
A3:
F is with_the_same_dom
and
A5:
for n being Nat holds G . n = (F . n) | E
; lim (Partial_Sums G) = (lim (Partial_Sums F)) | E
A6:
G is with_the_same_dom additive Functional_Sequence of X,ExtREAL
by A2, A3, A5, MESFUNC9:18, MESFUNC9:31;
dom ((F . 0) | E) = E
by A1, RELAT_1:62;
then A8:
E = dom (G . 0)
by A5;
A9:
for x being Element of X st x in E holds
F # x = G # x
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, MESFUNC9:29;
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 A6, MESFUNC9:29;
A22:
dom ((lim (Partial_Sums F)) | E) = E
by A14, RELAT_1:62;
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) = (lim (Partial_Sums F)) | E
by A8, A20, A13, A22, PARTFUN1:5; verum