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
B2: 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:
dom ((F . 0 ) | E) = E by A1, RELAT_1:91;
then P4: E = dom (G . 0 ) by A4;
let x be Element of X; :: thesis:
assume Q1: x in E ; :: thesis:
then F # x is summable by A3;
then Q3: Partial_Sums (F # x) is convergent by Def2;
for n being Element of NAT holds (F # x) . n = (G # x) . n

let n be Element of NAT ; :: thesis:
R11: (F # x) . n = (F . n) . x by MESFUNC5:def 13;
dom (G . n) = E by P4, B2, MESFUNC8:def 2;
then x in dom ((F . n) | E) by A4, Q1;
then ((F . n) | E) . x = (F . n) . x by FUNCT_1:70;
then (G . n) . x = (F . n) . x by A4;
hence (F # x) . n = (G # x) . n by R11, MESFUNC5:def 13; :: thesis:

end;

then Partial_Sums (F # x) = Partial_Sums (G # x) by FUNCT_2:113;
hence G # x is summable by Q3, Def2; :: thesis: