:: deftheorem defISO defines IsoCPRLSP LOPBAN12:def 1 :
for X, Y being RealLinearSpace
for b₃ being LinearOperator of [:X,Y:],(product <*X,Y*>) holds
( b₃ = IsoCPRLSP (X,Y) iff for x being Point of X
for y being Point of Y holds b₃ . (x,y) = <*x,y*> );