let X be non empty set ; :: thesis: for x being Element of X

for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds

(F || D) # x is convergent

let x be Element of X; :: thesis: for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds

(F || D) # x is convergent

let D be set ; :: thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds

(F || D) # x is convergent

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent implies (F || D) # x is convergent )

set G = F || D;

assume that

A1: F is with_the_same_dom and

A2: D c= dom (F . 0) and

A3: x in D ; :: thesis: ( not F # x is convergent or (F || D) # x is convergent )

Re (F || D) = (Re F) || D by Th21;

then A4: ( (Re F) # x is convergent implies (Re (F || D)) # x is convergent ) by A3, Th1;

dom ((Re F) . 0) = dom (F . 0) by MESFUN7C:def 11;

then dom (((Re F) . 0) | D) = D by A2, RELAT_1:62;

then dom ((Re (F || D)) . 0) = D by Lm1;

then A5: dom ((F || D) . 0) = D by MESFUN7C:def 11;

F || D is with_the_same_dom by A1, Th2;

then A6: ( (Re (F || D)) # x = Re ((F || D) # x) & (Im (F || D)) # x = Im ((F || D) # x) ) by A3, A5, MESFUN7C:23;

Im (F || D) = (Im F) || D by Th22;

then A7: ( (Im F) # x is convergent implies (Im (F || D)) # x is convergent ) by A3, Th1;

( (Re F) # x = Re (F # x) & (Im F) # x = Im (F # x) ) by A1, A2, A3, MESFUN7C:23;

hence ( not F # x is convergent or (F || D) # x is convergent ) by A4, A7, A6, COMSEQ_3:42; :: thesis: verum

for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds

(F || D) # x is convergent

let x be Element of X; :: thesis: for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds

(F || D) # x is convergent

let D be set ; :: thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds

(F || D) # x is convergent

let F be Functional_Sequence of X,COMPLEX; :: thesis: ( F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent implies (F || D) # x is convergent )

set G = F || D;

assume that

A1: F is with_the_same_dom and

A2: D c= dom (F . 0) and

A3: x in D ; :: thesis: ( not F # x is convergent or (F || D) # x is convergent )

Re (F || D) = (Re F) || D by Th21;

then A4: ( (Re F) # x is convergent implies (Re (F || D)) # x is convergent ) by A3, Th1;

dom ((Re F) . 0) = dom (F . 0) by MESFUN7C:def 11;

then dom (((Re F) . 0) | D) = D by A2, RELAT_1:62;

then dom ((Re (F || D)) . 0) = D by Lm1;

then A5: dom ((F || D) . 0) = D by MESFUN7C:def 11;

F || D is with_the_same_dom by A1, Th2;

then A6: ( (Re (F || D)) # x = Re ((F || D) # x) & (Im (F || D)) # x = Im ((F || D) # x) ) by A3, A5, MESFUN7C:23;

Im (F || D) = (Im F) || D by Th22;

then A7: ( (Im F) # x is convergent implies (Im (F || D)) # x is convergent ) by A3, Th1;

( (Re F) # x = Re (F # x) & (Im F) # x = Im (F # x) ) by A1, A2, A3, MESFUN7C:23;

hence ( not F # x is convergent or (F || D) # x is convergent ) by A4, A7, A6, COMSEQ_3:42; :: thesis: verum