a * (a *') = a .|. a by COMPLEX2:def 1
.= ((Re a) ^2) + ((Im a) ^2) by COMPLEX2:30 ;
hence a * (a *') is real ; :: thesis: verum