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 10;
then (F # x) . n = ((F . n) | E) . x by A2, FUNCT_1:49;
then (F # x) . n = ((F || E) . n) . x by Def1;
hence (F # x) . n = ((F || E) # x) . n by SEQFUNC:def 10; :: thesis: verum

end;

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