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
A5: F || E is with_the_same_dom by A2, Th8a;
B31: 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 P01: 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, P01, A2, MESFUN7C:23; :: thesis: verum

end;

B32: 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 P01: 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, P01, A2, 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 P01: x in E ; :: thesis: (F || E) # x is summable
(F || E) . 0 = (F . 0 ) | E by Def1;
then P03: x in dom ((F || E) . 0 ) by P01, A1, RELAT_1:91;
( Re (F || E) = (Re F) || E & Im (F || E) = (Im F) || E ) by Lm31, Lm32;
then ( (Re (F || E)) # x is summable & (Im (F || E)) # x is summable ) by P01, B31, B32, Th10;
then ( Re ((F || E) # x) is summable & Im ((F || E) # x) is summable ) by P03, A5, MESFUN7C:23;
hence (F || E) # x is summable by COMSEQ_3:58; :: thesis: verum

end;