:: deftheorem def2 defines *' DUALSP01:def 5 :
for V being RealLinearSpace
for b₂ being strict RealLinearSpace holds
( b₂ = V *' iff ex X being VectSp of F_Real st
( X = RLSp2RVSp V & b₂ = RVSp2RLSp (X *') ) );