theorem :: MESFUN9C:26

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