let a, b be Element of F_Real; :: thesis: ( a <> 0. F_Real implies ex x being Element of F_Real st a * x = b )

assume A1: a <> 0. F_Real ; :: thesis: ex x being Element of F_Real st a * x = b

reconsider p = a, q = b as Element of REAL by VECTSP_1:def 5;

reconsider x = q / p as Element of F_Real by VECTSP_1:def 5;

p * (q / p) = q by A1, Lm1, XCMPLX_1:87;

then a * x = b ;

hence ex x being Element of F_Real st a * x = b ; :: thesis: verum

assume A1: a <> 0. F_Real ; :: thesis: ex x being Element of F_Real st a * x = b

reconsider p = a, q = b as Element of REAL by VECTSP_1:def 5;

reconsider x = q / p as Element of F_Real by VECTSP_1:def 5;

p * (q / p) = q by A1, Lm1, XCMPLX_1:87;

then a * x = b ;

hence ex x being Element of F_Real st a * x = b ; :: thesis: verum