:: deftheorem Def1 defines Exch NDIFF10:def 1 :
for X, Y being RealNormSpace
for b₃ being LinearOperator of [:X,Y:],[:Y,X:] holds
( b₃ = Exch (X,Y) iff ( b₃ is one-to-one & b₃ is onto & b₃ is isometric & ( for x being Point of X
for y being Point of Y holds b₃ . (x,y) = [y,x] ) ) );