:: deftheorem defines isomorphism NORMSP_3:def 10 :
for X, Y being RealLinearSpace
for L being LinearOperator of X,Y holds
( L is isomorphism iff ( L is one-to-one & L is onto ) );