theorem Th1: :: MESFUN9C:1

for X being non empty set
for F being Functional_Sequence of X,REAL
for x being Element of X
for D being set st x in D & F # x is convergent holds
(F || D) # x is convergent