for D being non empty set
for H being Functional_Sequence of D,REAL
for X being set st H is_point_conv_on X holds
( abs H is_point_conv_on X & lim ((abs H),X) = |.(lim (H,X)).| & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) )