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
A0: F is with_the_same_dom and
A1: 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 & Im (F || D) = (Im F) || D ) by Lm31, Lm32;
then B3: ( ( (Re F) # x is convergent implies (Re (F || D)) # x is convergent ) & ( (Im F) # x is convergent implies (Im (F || D)) # x is convergent ) ) by A3, Th4;
dom ((Re F) . 0 ) = dom (F . 0 ) by MESFUN7C:def 11;
then dom (((Re F) . 0 ) | D) = D by A1, RELAT_1:91;
then dom ((Re (F || D)) . 0 ) = D by Lem30;
then B6: dom ((F || D) . 0 ) = D by MESFUN7C:def 11;
F || D is with_the_same_dom by A0, Th8a;
then ( (Re F) # x = Re (F # x) & (Im F) # x = Im (F # x) & (Re (F || D)) # x = Re ((F || D) # x) & (Im (F || D)) # x = Im ((F || D) # x) ) by A0, A1, A3, B6, MESFUN7C:23;
hence ( not F # x is convergent or (F || D) # x is convergent ) by B3, COMSEQ_3:42; :: thesis: verum