theorem Th18: :: SEQFUNC:19

for D being non empty set
for H being Functional_Sequence of D,REAL
for X being set holds
( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D,REAL st
( X = dom f & ( for x being Element of D st x in X holds
( H # x is convergent & lim (H # x) = f . x ) ) ) ) )