:: deftheorem Def7 defines scalar-conjugative CAYLDICK:def 7 :
for N being non empty ConjNormAlgStr holds
( N is scalar-conjugative iff for r being Real
for a being Element of N holds r * (a *') = (r * a) *' );