:: deftheorem Def1 defines IsoCPRLSP LOPBAN14:def 1 :
for X being RealLinearSpace
for b₂ being LinearOperator of X,(product <*X*>) holds
( b₂ = IsoCPRLSP X iff for x being Point of X holds b₂ . x = <*x*> );