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
A1: F is with_the_same_dom and
A2: 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: Re (F || D) = (Re F) || D by Th21;

A5: now :: thesis: for x being Element of X st x in dom ((F || D) . 0) holds
(F || D) # x is convergent

let x be Element of X; :: thesis: ( x in dom ((F || D) . 0) implies (F || D) # x is convergent )
dom ((F . 0) | D) = D by A2, RELAT_1:62;
then A6: dom ((F || D) . 0) = D by Def1;
assume A7: x in dom ((F || D) . 0) ; :: thesis: (F || D) # x is convergent
then F # x is convergent by A3, A6;
hence (F || D) # x is convergent by A1, A2, A7, A6, Th23; :: thesis: verum

end;

A8: 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 A9: 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 A1, A2, A9, MESFUN7C:23; :: thesis: verum

end;

D c= dom ((Re F) . 0) by A2, MESFUN7C:def 11;
then (lim (Re F)) | D = lim (Re (F || D)) by A4, A8, Th3;
then A10: (Re (lim F)) | D = lim (Re (F || D)) by A1, A2, A3, MESFUN7C:25;
A11: F || D is with_the_same_dom by A1, Th2;
then lim (Re (F || D)) = Re (lim (F || D)) by A5, MESFUN7C:25;
then A12: Re ((lim F) | D) = Re (lim (F || D)) by A10, Th20;
A13: 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 A14: 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 A1, A2, A14, MESFUN7C:23; :: thesis: verum

end;

A15: Im (F || D) = (Im F) || D by Th22;
D c= dom ((Im F) . 0) by A2, MESFUN7C:def 12;
then (lim (Im F)) | D = lim (Im (F || D)) by A15, A13, Th3;
then A16: (Im (lim F)) | D = lim (Im (F || D)) by A1, A2, A3, MESFUN7C:25;
lim (Im (F || D)) = Im (lim (F || D)) by A11, A5, MESFUN7C:25;
then A17: Im ((lim F) | D) = Im (lim (F || D)) by A16, Th20;
thus lim (F || D) = (Re (lim (F || D))) + (<i> (#) (Im (lim (F || D)))) by MESFUN6C:8
.= (lim F) | D by A12, A17, MESFUN6C:8 ; :: thesis: verum