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 () = (lim ()) | 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 () = (lim ()) | 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 () = (lim ()) | 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 () = (lim ()) | E )
assume that
A1: E c= dom (F . 0) and
A3: F is with_the_same_dom and
A5: for n being Nat holds G . n = (F . n) | E ; :: thesis: lim () = (lim ()) | E
A6: G is with_the_same_dom additive Functional_Sequence of X,ExtREAL by ;
dom ((F . 0) | E) = E by ;
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 ;
then x in dom ((F . n) | E) by ;
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 ; :: 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 ()) = dom (() . 0) by MESFUNC8:def 9;
dom (() . 0) = dom (F . 0) by ;
then A14: E c= dom (lim ()) by ;
A15: for x being Element of X st x in dom (lim ()) holds
(lim ()) . x = (lim ()) . x
proof
let x be Element of X; :: thesis: ( x in dom (lim ()) implies (lim ()) . x = (lim ()) . x )
set PFx = Partial_Sums (F # x);
set PGx = Partial_Sums (G # x);
assume A16: x in dom (lim ()) ; :: thesis: (lim ()) . x = (lim ()) . x
then x in dom (G . 0) by ;
then x in dom ((F . 0) | E) by A5;
then A17: x in E by ;
for n being Element of NAT holds (() # x) . n = (() # x) . n
proof
let n be Element of NAT ; :: thesis: (() # x) . n = (() # x) . n
A18: (Partial_Sums (G # x)) . n = (() # x) . n by ;
(Partial_Sums (F # x)) . n = (() # x) . n by ;
hence ((Partial_Sums G) # x) . n = (() # x) . n by A9, A17, A18; :: thesis: verum
end;
then A19: lim (() # x) = lim (() # x) by FUNCT_2:63;
(lim ()) . x = lim (() # x) by ;
hence (lim ()) . x = (lim ()) . x by ; :: thesis: verum
end;
A20: dom (() . 0) = dom (G . 0) by ;
A22: dom ((lim ()) | E) = E by ;
for x being Element of X st x in dom ((lim ()) | E) holds
((lim ()) | E) . x = ((lim ()) | E) . x
proof
let x be Element of X; :: thesis: ( x in dom ((lim ()) | E) implies ((lim ()) | E) . x = ((lim ()) | E) . x )
assume A24: x in dom ((lim ()) | E) ; :: thesis: ((lim ()) | E) . x = ((lim ()) | E) . x
then ((lim ()) | E) . x = (lim ()) . x by ;
hence ((lim ()) | E) . x = ((lim ()) | E) . x by A8, A13, A20, A15, A24; :: thesis: verum
end;
hence lim () = (lim ()) | E by ; :: thesis: verum