for X, Y being RealNormSpace
for L being Lipschitzian LinearOperator of X,Y
for seq being sequence of X st L is isomorphism holds
( seq is Cauchy_sequence_by_Norm iff L * seq is Cauchy_sequence_by_Norm )