let z be non zero Complex; :: thesis: ((1 / z) ^2) * (z ^2) = 1
((1 / z) ^2) * (z ^2) = ((1 / z) * ((1 / z) * z)) * z
.= ((1 / z) * 1) * z by XCMPLX_1:106
.= 1 by XCMPLX_1:106 ;
hence ((1 / z) ^2) * (z ^2) = 1 ; :: thesis: verum