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) ) )
dom (lim (Re f)) = dom ((Re f) . 0) by MESFUNC8:def 9;
then A1: dom (lim (Re f)) = dom (f . 0) by Def11;
A2: dom (Re (lim f)) = dom (lim f) by COMSEQ_3:def 3;
then A3: dom (lim (Re f)) = dom (Re (lim f)) by A1, Def10;
assume A4: 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) )

A5: now :: thesis: for x being Element of X st x in dom (lim (Re f)) holds
(lim (Re f)) . x = (Re (lim f)) . x

let x be Element of X; :: thesis: ( x in dom (lim (Re f)) implies (lim (Re f)) . x = (Re (lim f)) . x )
assume A6: x in dom (lim (Re f)) ; :: thesis: (lim (Re f)) . x = (Re (lim f)) . x
then A7: f # x is convergent by A4, A1;
then Re (f # x) is convergent ;
then A8: (Re f) # x is convergent by A1, A6, Th23;
(lim (Re f)) . x = lim (R_EAL ((Re f) # x)) by A6, Th14
.= lim ((Re f) # x) by A8, RINFSUP2:14 ;
then (lim (Re f)) . x = lim (Re (f # x)) by A1, A6, Th23;
then A9: (lim (Re f)) . x = Re (lim (f # x)) by A7, COMSEQ_3:41;
(Re (lim f)) . x = Re ((lim f) . x) by A3, A6, COMSEQ_3:def 3;
hence (lim (Re f)) . x = (Re (lim f)) . x by A2, A3, A6, A9, Def10; :: thesis: verum

end;

Re (lim f) is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7;
hence lim (Re f) = Re (lim f) by A3, A5, PARTFUN1:5; :: thesis: lim (Im f) = Im (lim f)
dom (lim (Im f)) = dom ((Im f) . 0) by MESFUNC8:def 9;
then A10: dom (lim (Im f)) = dom (f . 0) by Def12;
A11: dom (Im (lim f)) = dom (lim f) by COMSEQ_3:def 4;
then A12: dom (lim (Im f)) = dom (Im (lim f)) by A10, Def10;

A13: now :: thesis: for x being Element of X st x in dom (lim (Im f)) holds
(lim (Im f)) . x = (Im (lim f)) . x

let x be Element of X; :: thesis: ( x in dom (lim (Im f)) implies (lim (Im f)) . x = (Im (lim f)) . x )
assume A14: x in dom (lim (Im f)) ; :: thesis: (lim (Im f)) . x = (Im (lim f)) . x
then A15: f # x is convergent by A4, A10;
then Im (f # x) is convergent ;
then A16: (Im f) # x is convergent by A10, A14, Th23;
(lim (Im f)) . x = lim (R_EAL ((Im f) # x)) by A14, Th14
.= lim ((Im f) # x) by A16, RINFSUP2:14 ;
then (lim (Im f)) . x = lim (Im (f # x)) by A10, A14, Th23;
then A17: (lim (Im f)) . x = Im (lim (f # x)) by A15, COMSEQ_3:41;
(Im (lim f)) . x = Im ((lim f) . x) by A12, A14, COMSEQ_3:def 4;
hence (lim (Im f)) . x = (Im (lim f)) . x by A11, A12, A14, A17, Def10; :: thesis: verum

end;

Im (lim f) is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7;
hence lim (Im f) = Im (lim f) by A12, A13, PARTFUN1:5; :: thesis: verum