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