theorem :: SEQFUNC2:17

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 st H is_point_conv_on X holds
for x being set st x in X holds
{x} common_on_dom H by Th25;