:: deftheorem defines *' CAYLDICK:def 2 :
for N being non empty ConjNormAlgStr
for a being Element of N holds a *' = the conjugateF of N . a;