theorem NISOM04: :: NORMSP_3:42

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