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

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

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

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

set E1 = dom (F . 0);
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

end;assume A10: x in E ; :: thesis: F # x = G # x

for n being Element of NAT holds (F # x) . n = (G # x) . n

proof

hence
F # x = G # x
by FUNCT_2:def 7; :: thesis: verum
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;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

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

A20:
dom ((Partial_Sums G) . 0) = dom (G . 0)
by A6, MESFUNC9:29;
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

(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;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

then A19:
lim ((Partial_Sums G) # x) = lim ((Partial_Sums F) # x)
by FUNCT_2:63;
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;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

(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

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

hence
lim (Partial_Sums G) = (lim (Partial_Sums F)) | E
by A8, A20, A13, A22, PARTFUN1:5; :: thesis: verum
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;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