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,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
let S be SigmaField of X; :: thesis: 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
let E be Element of S; :: thesis: 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
let F be Functional_Sequence of X,COMPLEX; :: thesis: ( 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 ) implies for x being Element of X st x in E holds
(F || E) # x is summable )
set G = F || E;
assume that
A1: E c= dom (F . 0) and
A2: F is with_the_same_dom and
A3: 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
A4: F || E is with_the_same_dom by A2, Th2;
A5: for x being Element of X st x in E holds
(Im F) # x is summable

proof

let x be Element of X; :: thesis: ( x in E implies (Im F) # x is summable )
assume A6: x in E ; :: thesis: (Im F) # x is summable
then F # x is summable by A3;
then Im (F # x) is summable ;
hence (Im F) # x is summable by A1, A2, A6, MESFUN7C:23; :: thesis: verum

end;

A7: for x being Element of X st x in E holds
(Re F) # x is summable

proof

let x be Element of X; :: thesis: ( x in E implies (Re F) # x is summable )
assume A8: x in E ; :: thesis: (Re F) # x is summable
then F # x is summable by A3;
then Re (F # x) is summable ;
hence (Re F) # x is summable by A1, A2, A8, MESFUN7C:23; :: thesis: verum

end;

hereby :: thesis: verum

let x be Element of X; :: thesis: ( x in E implies (F || E) # x is summable )
assume A9: x in E ; :: thesis: (F || E) # x is summable
(F || E) . 0 = (F . 0) | E by Def1;
then A10: x in dom ((F || E) . 0) by A1, A9, RELAT_1:62;
Im (F || E) = (Im F) || E by Th22;
then (Im (F || E)) # x is summable by A5, A9, Th6;
then A11: Im ((F || E) # x) is summable by A4, A10, MESFUN7C:23;
Re (F || E) = (Re F) || E by Th21;
then (Re (F || E)) # x is summable by A7, A9, Th6;
then Re ((F || E) # x) is summable by A4, A10, MESFUN7C:23;
hence (F || E) # x is summable by A11, COMSEQ_3:57; :: thesis: verum

end;