reconsider b = x " as Element of F_Rat by RAT_1:def 2;
assume A1: x = a ; :: thesis: / a = x "
A2: a <> 0. F_Rat ;
then b * a = 1. F_Rat by A1, XCMPLX_0:def 7;
hence / a = x " by A2, VECTSP_1:def 10; :: thesis: verum