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
( ||.H.|| is_point_conv_on X & lim (||.H.||,X) = ||.(lim (H,X)).|| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )