for N being non empty ConjNormAlgStr st N is add-associative & N is right_zeroed & N is right_complementable & N is well-conjugated & N is reflexive & N is scalar-distributive & N is scalar-unital & N is vector-distributive & N is left-distributive holds
for a being Element of N holds (a *') * a = (||.a.|| ^2) * (1. N)