let X be non empty set ; :: thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX st ( for x being Element of X st x in dom (f . 0 ) holds
f # x is convergent ) holds
( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )
let f be with_the_same_dom Functional_Sequence of X,COMPLEX ; :: thesis: ( ( for x being Element of X st x in dom (f . 0 ) holds
f # x is convergent ) implies ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) ) )
assume A2: for x being Element of X st x in dom (f . 0 ) holds
f # x is convergent ; :: thesis: ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )
dom (lim (Re f)) = dom ((Re f) . 0 ) by MESFUNC8:def 10;
then P1: dom (lim (Re f)) = dom (f . 0 ) by Def13;
P2: dom (Re (lim f)) = dom (lim f) by MESFUN6C:def 1;
then B1: dom (lim (Re f)) = dom (Re (lim f)) by P1, Def12;
dom (lim (Im f)) = dom ((Im f) . 0 ) by MESFUNC8:def 10;
then Q1: dom (lim (Im f)) = dom (f . 0 ) by Def14;
Q2: dom (Im (lim f)) = dom (lim f) by MESFUN6C:def 2;
then B2: dom (lim (Im f)) = dom (Im (lim f)) by Q1, Def12;

P00: now

let x be Element of X; :: thesis: ( x in dom (lim (Re f)) implies (lim (Re f)) . x = (Re (lim f)) . x )
assume P01: x in dom (lim (Re f)) ; :: thesis: (lim (Re f)) . x = (Re (lim f)) . x
then C1: f # x is convergent by A2, P1;
then Re (f # x) is convergent ;
then PP: (Re f) # x is convergent by P01, P1, Th7a;
(lim (Re f)) . x = lim (R_EAL ((Re f) # x)) by P01, Def10a
.= lim ((Re f) # x) by PP, RINFSUP2:14 ;
then (lim (Re f)) . x = lim (Re (f # x)) by P01, P1, Th7a;
then P03: (lim (Re f)) . x = Re (lim (f # x)) by C1, COMSEQ_3:41;
(Re (lim f)) . x = Re ((lim f) . x) by P01, B1, MESFUN6C:def 1;
hence (lim (Re f)) . x = (Re (lim f)) . x by P03, P01, B1, P2, Def12; :: thesis: verum

end;

Re (lim f) is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:17;
hence lim (Re f) = Re (lim f) by B1, P00, PARTFUN1:34; :: thesis: lim (Im f) = Im (lim f)

P00: now

let x be Element of X; :: thesis: ( x in dom (lim (Im f)) implies (lim (Im f)) . x = (Im (lim f)) . x )
assume P01: x in dom (lim (Im f)) ; :: thesis: (lim (Im f)) . x = (Im (lim f)) . x
then D1: f # x is convergent by A2, Q1;
then Im (f # x) is convergent ;
then PP: (Im f) # x is convergent by P01, Q1, Th7a;
(lim (Im f)) . x = lim (R_EAL ((Im f) # x)) by P01, Def10a
.= lim ((Im f) # x) by PP, RINFSUP2:14 ;
then (lim (Im f)) . x = lim (Im (f # x)) by P01, Q1, Th7a;
then P03: (lim (Im f)) . x = Im (lim (f # x)) by D1, COMSEQ_3:41;
(Im (lim f)) . x = Im ((lim f) . x) by P01, B2, MESFUN6C:def 2;
hence (lim (Im f)) . x = (Im (lim f)) . x by P03, P01, B2, Q2, Def12; :: thesis: verum

end;

Im (lim f) is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:17;
hence lim (Im f) = Im (lim f) by B2, P00, PARTFUN1:34; :: thesis: verum