for X, Y being RealNormSpace
for f being LinearOperator of X,Y holds
( f is Lipschitzian iff f is_continuous_on the carrier of X )