theorem Th25: :: MESFUN7C:25

for X being non empty set
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) )