for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,COMPLEX st E c= dom (F . 0) & F is with_the_same_dom & ( 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