let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
let S be SigmaField of X; :: thesis: for E being Element of S
for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
let E be Element of S; :: thesis: for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds
F # x is summable ) holds
for x being Element of X st x in E holds
(F || E) # x is summable
let F be Functional_Sequence of X,REAL ; :: thesis: ( ( for x being Element of X st x in E holds
F # x is summable ) implies for x being Element of X st x in E holds
(F || E) # x is summable )
set G = F || E;
assume A1: for x being Element of X st x in E holds
F # x is summable ; :: thesis: for x being Element of X st x in E holds
(F || E) # x is summable
let x be Element of X; :: thesis: ( x in E implies (F || E) # x is summable )
assume A2: x in E ; :: thesis: (F || E) # x is summable
for n being Element of NAT holds (F # x) . n = ((F || E) # x) . n

proof

let n be Element of NAT ; :: thesis: (F # x) . n = ((F || E) # x) . n
(F # x) . n = (F . n) . x by SEQFUNC:def 11;
then (F # x) . n = ((F . n) | E) . x by A2, FUNCT_1:72;
then (F # x) . n = ((F || E) . n) . x by Def1;
hence (F # x) . n = ((F || E) # x) . n by SEQFUNC:def 11; :: thesis: verum

end;

then A3: Partial_Sums (F # x) = Partial_Sums ((F || E) # x) by FUNCT_2:113;
F # x is summable by A1, A2;
then Partial_Sums (F # x) is convergent by SERIES_1:def 2;
hence (F || E) # x is summable by A3, SERIES_1:def 2; :: thesis: verum