:: deftheorem Def2 defines IsoCPNrSP LOPBAN14:def 2 :
for X being RealNormSpace
for b₂ being LinearOperator of X,(product <*X*>) holds
( b₂ = IsoCPNrSP X iff for x being Point of X holds b₂ . x = <*x*> );