:: deftheorem defines isomorphism NORMSP_3:def 11 :
for X, Y being RealNormSpace
for L being LinearOperator of X,Y holds
( L is isomorphism iff ( L is one-to-one & L is onto & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) ) );