let a be Complex; :: thesis: a * (a *') = |.a.| ^2
set ac = a;
reconsider b = a *' as Complex ;
reconsider Ra = Re a, Ia = Im a as Real ;
reconsider Ra2 = Ra ^2 , Ia2 = Ia ^2 as Real ;
A1: |.a.| = sqrt (Ra2 + Ia2) by COMPLEX1:def 12;
reconsider xx = Ra2 + Ia2 as Real ;
( Ra2 >= 0 & 0 <= Ia2 ) by XREAL_1:63;
then |.a.| ^2 = (((Re a) * (Re a)) - ((Im a) * (- (Im a)))) + ((((Re a) * (- (Im a))) + ((Re a) * (Im a))) * <i>) by A1, SQUARE_1:def 2
.= (((Re a) * (Re a)) - ((Im a) * (- (Im a)))) + ((((Re a) * (Im b)) + ((Re a) * (Im a))) * <i>) by COMPLEX1:27
.= (((Re a) * (Re a)) - ((Im a) * (Im b))) + ((((Re a) * (Im b)) + ((Re a) * (Im a))) * <i>) by COMPLEX1:27
.= (((Re a) * (Re a)) - ((Im a) * (Im b))) + ((((Re a) * (Im b)) + ((Re b) * (Im a))) * <i>) by COMPLEX1:27
.= (((Re a) * (Re b)) - ((Im a) * (Im b))) + ((((Re a) * (Im b)) + ((Re b) * (Im a))) * <i>) by COMPLEX1:27
.= a * b by COMPLEX1:82 ;
hence a * (a *') = |.a.| ^2 ; :: thesis: verum