theorem :: NORMSP_3:44

for X, Y being RealNormSpace st ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism holds
( X is complete iff Y is complete )