let X be non empty set ; :: thesis: for D being set
for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0 ) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim (F || D)
let D be set ; :: thesis: for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0 ) & ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim (F || D)
let F be Functional_Sequence of X,COMPLEX ; :: thesis: ( F is with_the_same_dom & D = dom (F . 0 ) & ( for x being Element of X st x in D holds
F # x is convergent ) implies (lim F) | D = lim (F || D) )
set G = F || D;
assume that
A0: F is with_the_same_dom and
A1: D = dom (F . 0 ) and
A3: for x being Element of X st x in D holds
F # x is convergent ; :: thesis: (lim F) | D = lim (F || D)
A4: F || D is with_the_same_dom by A0, Th8a;
B1: ( D c= dom ((Re F) . 0 ) & D c= dom ((Im F) . 0 ) ) by A1, MESFUN7C:def 11, MESFUN7C:def 12;
b2: ( Re (F || D) = (Re F) || D & Im (F || D) = (Im F) || D ) by Lm31, Lm32;
B4: for x being Element of X st x in D holds
(Re F) # x is convergent

proof

let x be Element of X; :: thesis: ( x in D implies (Re F) # x is convergent )
assume P01: x in D ; :: thesis: (Re F) # x is convergent
then F # x is convergent Complex_Sequence by A3;
then Re (F # x) is convergent ;
hence (Re F) # x is convergent by A0, P01, A1, MESFUN7C:23; :: thesis: verum

end;

for x being Element of X st x in D holds
(Im F) # x is convergent

proof

let x be Element of X; :: thesis: ( x in D implies (Im F) # x is convergent )
assume P01: x in D ; :: thesis: (Im F) # x is convergent
then F # x is convergent Complex_Sequence by A3;
then Im (F # x) is convergent ;
hence (Im F) # x is convergent by A0, P01, A1, MESFUN7C:23; :: thesis: verum

end;

then ( (lim (Re F)) | D = lim (Re (F || D)) & (lim (Im F)) | D = lim (Im (F || D)) ) by B1, b2, B4, Th919r;
then C4: ( (Re (lim F)) | D = lim (Re (F || D)) & (Im (lim F)) | D = lim (Im (F || D)) ) by A0, A1, A3, MESFUN7C:25;

now

let x be Element of X; :: thesis: ( x in dom ((F || D) . 0 ) implies (F || D) # x is convergent )
assume P01: x in dom ((F || D) . 0 ) ; :: thesis: (F || D) # x is convergent
dom ((F . 0 ) | D) = D by A1, RELAT_1:91;
then P03: dom ((F || D) . 0 ) = D by Def1;
then F # x is convergent by A3, P01;
hence (F || D) # x is convergent by P01, P03, A0, A1, M9C32c; :: thesis: verum

end;

then ( lim (Re (F || D)) = Re (lim (F || D)) & lim (Im (F || D)) = Im (lim (F || D)) ) by A4, MESFUN7C:25;
then C3: ( Re ((lim F) | D) = Re (lim (F || D)) & Im ((lim F) | D) = Im (lim (F || D)) ) by C4, MES6C7;
thus lim (F || D) = (Re (lim (F || D))) + (<i> (#) (Im (lim (F || D)))) by MESFUN6C:8
.= (lim F) | D by C3, MESFUN6C:8 ; :: thesis: verum