theorem Th3: :: MESFUN9C:3

for X being non empty set
for F being Functional_Sequence of X,REAL
for D being set st D c= 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)