let a, b be Real; :: thesis: (a ^2) * (1 / (b ^2)) = (a / b) ^2
(a ^2) * (1 / (b ^2)) = (a * a) * ((1 / b) * (1 / b)) by XCMPLX_1:102
.= (a * (a * (1 / b))) * (1 / b)
.= (a * ((a * 1) / b)) * (1 / b) by XCMPLX_1:74
.= (a / b) * (a * (1 / b))
.= (a / b) * ((a * 1) / b) by XCMPLX_1:74
.= (a / b) ^2 ;
hence (a ^2) * (1 / (b ^2)) = (a / b) ^2 ; :: thesis: verum