let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for F, G being Functional_Sequence of X,ExtREAL st E c= dom (F . 0) & G is with_the_same_dom & ( for x being Element of X st x in E holds
F # x is summable ) & ( for n being Nat holds G . n = (F . n) | E ) holds
for x being Element of X st x in E holds
G # x is summable
let S be SigmaField of X; :: thesis: for E being Element of S
for F, G being Functional_Sequence of X,ExtREAL st E c= dom (F . 0) & G is with_the_same_dom & ( for x being Element of X st x in E holds
F # x is summable ) & ( for n being Nat holds G . n = (F . n) | E ) holds
for x being Element of X st x in E holds
G # x is summable
let E be Element of S; :: thesis: for F, G being Functional_Sequence of X,ExtREAL st E c= dom (F . 0) & G is with_the_same_dom & ( for x being Element of X st x in E holds
F # x is summable ) & ( for n being Nat holds G . n = (F . n) | E ) holds
for x being Element of X st x in E holds
G # x is summable
let F, G be Functional_Sequence of X,ExtREAL; :: thesis: ( E c= dom (F . 0) & G is with_the_same_dom & ( for x being Element of X st x in E holds
F # x is summable ) & ( for n being Nat holds G . n = (F . n) | E ) implies for x being Element of X st x in E holds
G # x is summable )
assume that
A1: E c= dom (F . 0) and
A2: G is with_the_same_dom and
A3: for x being Element of X st x in E holds
F # x is summable and
A4: for n being Nat holds G . n = (F . n) | E ; :: thesis: for x being Element of X st x in E holds
G # x is summable
let x be Element of X; :: thesis: ( x in E implies G # x is summable )
assume A5: x in E ; :: thesis: G # x is summable
dom ((F . 0) | E) = E by A1, RELAT_1:62;
then A6: E = dom (G . 0) by A4;
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 A2, A6;
then x in dom ((F . n) | E) by A4, A5;
then ((F . n) | E) . x = (F . n) . x by FUNCT_1:47;
then A7: (G . n) . x = (F . n) . x by A4;
(F # x) . n = (F . n) . x by MESFUNC5:def 13;
hence (F # x) . n = (G # x) . n by A7, MESFUNC5:def 13; :: thesis: verum

end;

then A8: Partial_Sums (F # x) = Partial_Sums (G # x) by FUNCT_2:63;
F # x is summable by A3, A5;
then Partial_Sums (F # x) is convergent ;
hence G # x is summable by A8; :: thesis: verum