let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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
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 n being Element of NAT holds (F # x) . n = (G # x) . n
proof
let n be Element of NAT ; :: thesis: (F # x) . n = (G # x) . n
dom (G . n) = E by A8, MESFUNC8:def 2, A3, A5, MESFUNC9:18;
then x in dom ((F . n) | E) by A5, A10;
then ((F . n) | E) . x = (F . n) . x by FUNCT_1:47;
then A11: (G . n) . x = (F . n) . x by A5;
(F # x) . n = (F . n) . x by MESFUNC5:def 13;
hence (F # x) . n = (G # x) . n by A11, MESFUNC5:def 13; :: thesis: verum
end;
hence F # x = G # x by FUNCT_2:def 7; :: thesis: verum
end;
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
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 x in dom (G . 0) by A6, A13, MESFUNC9:29;
then x in dom ((F . 0) | E) by A5;
then A17: x in E by A1, RELAT_1:62;
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 A6, A8, A17, MESFUNC9:32;
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n by A1, A2, A3, A17, MESFUNC9:32;
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 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
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 ((lim (Partial_Sums F)) | E) . x = (lim (Partial_Sums F)) . x by A8, A13, A20, A22, FUNCT_1:47;
hence ((lim (Partial_Sums G)) | E) . x = ((lim (Partial_Sums F)) | E) . x by A8, A13, A20, A15, A24; :: thesis: verum
end;
hence lim (Partial_Sums G) = (lim (Partial_Sums F)) | E by A8, A20, A13, A22, PARTFUN1:5; :: thesis: verum