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