reconsider b = x " as Element of F_Real by XREAL_0:def 1;
A1: a <> 0. F_Real ;
assume x = a ; :: thesis: a " = x "
then b * a = 1. F_Real by A1, XCMPLX_0:def 7;
hence a " = x " by A1, Def10; :: thesis: verum