for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set holds
( H is_point_conv_on X iff ( X common_on_dom H & ( for x being Element of D st x in X holds
H # x is convergent ) ) )