let a be Integer; :: thesis: |.a.| |^ 2 = a |^ 2
thus |.a.| |^ 2 = |.a.| ^2
.= a ^2 by COMPLEX1:75
.= a |^ 2 ; :: thesis: verum