let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let E be Element of S; :: thesis:
let F, G be Functional_Sequence of X,ExtREAL; :: thesis:
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:
let x be Element of X; :: thesis:
assume A5: x in E ; :: thesis:
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

let n be Element of NAT ; :: thesis:
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:

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: