theorem Th25: :: SEQFUNC:26

for D being non empty set
for H being Functional_Sequence of D,REAL
for X being set st X common_on_dom H holds
for x being Element of D st x in X holds
{x} common_on_dom H