for a being Element of COMPLEX holds a * (a *') = (|.a.| ^2) + (0 * <i>)