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

(Re F) # x is summable

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

A7:
for x being Element of X st x in E holds
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;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

(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;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

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;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