theorem :: NDIFF11:1

for n being non zero Nat
for X being RealNormSpace
for f being LinearOperator of (REAL-NS n),X holds f is Lipschitzian