:: deftheorem Def5 defines add-conjugative CAYLDICK:def 5 :
for N being non empty ConjNormAlgStr holds
( N is add-conjugative iff for a, b being Element of N holds (a + b) *' = (a *') + (b *') );