for X, Y being RealNormSpace
for f being Lipschitzian LinearOperator of X,Y holds
( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )