let r be Real; :: thesis: ( r <> 0 implies [\(r / r)/] = 1 )
assume r <> 0 ; :: thesis: [\(r / r)/] = 1
hence [\(r / r)/] = [\1/] by XCMPLX_1:60
.= 1 ;
:: thesis: verum