theorem :: CAYLDICK:11

for N being non empty ConjNormAlgStr
for a, b being Element of N st N is well-conjugated & N is reflexive & N is discerning & N is RealNormSpace-like & N is vector-distributive & N is scalar-distributive & N is scalar-associative & N is scalar-unital & N is Abelian & N is add-associative & N is right_zeroed & N is right_complementable & N is associative & N is distributive & N is well-unital & not N is degenerated & N is almost_left_invertible & N is add-conjugative holds
(a - b) *' = (a *') - (b *')