let a be Element of N_Real; :: thesis: a * a = ||.a.|| ^2
reconsider x = a as Element of REAL ;
thus a * a = x ^2
.= ||.a.|| ^2 by COMPLEX1:75 ; :: thesis: verum