:: deftheorem defISO defines IsoCPNrSP NDIFF_7:def 3 :
for X, Y being RealNormSpace
for b₃ being LinearOperator of [:X,Y:],(product <*X,Y*>) holds
( b₃ = IsoCPNrSP (X,Y) iff for x being Point of X
for y being Point of Y holds b₃ . (x,y) = <*x,y*> );