for X being RealNormSpace holds id the carrier of X is Lipschitzian LinearOperator of X,X