assume A1: a = r ; :: thesis: / a = r "
reconsider b = r " as Element of N_Real by XREAL_0:def 1;
A2: a <> 0. N_Real ;
then b * a = 1. N_Real by A1, XCMPLX_0:def 7;
hence / a = r " by A2, VECTSP_2:def 2; :: thesis: verum