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 ;
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
.= lim ((Re f) # x) by ;
then (lim (Re f)) . x = lim (Re (f # x)) by A1, A6, Th23;
then A9: (lim (Re f)) . x = Re (lim (f # x)) by ;
(Re (lim f)) . x = Re ((lim f) . x) by ;
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 ;
hence lim (Re f) = Re (lim f) by ; :: 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 ;
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 ;
then Im (f # x) is convergent ;
then A16: (Im f) # x is convergent by ;
(lim (Im f)) . x = lim (R_EAL ((Im f) # x)) by
.= lim ((Im f) # x) by ;
then (lim (Im f)) . x = lim (Im (f # x)) by ;
then A17: (lim (Im f)) . x = Im (lim (f # x)) by ;
(Im (lim f)) . x = Im ((lim f) . x) by ;
hence (lim (Im f)) . x = (Im (lim f)) . x by ; :: thesis: verum
end;
Im (lim f) is PartFunc of X,ExtREAL by ;
hence lim (Im f) = Im (lim f) by ; :: thesis: verum