:: deftheorem Def3 defines well-conjugated CAYLDICK:def 3 :
for N being non empty ConjNormAlgStr
for a being Element of N holds
( ( not a is zero implies ( a is well-conjugated iff (a *') * a = (||.a.|| ^2) * (1. N) ) ) & ( a is zero implies ( a is well-conjugated iff a *' is zero ) ) );