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

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

reconsider p = a, q = b as Element of REAL ;

reconsider x = q / p as Element of multEX_0 ;

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

then x * a = b by BINOP_2:def 11;

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

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

reconsider p = a, q = b as Element of REAL ;

reconsider x = q / p as Element of multEX_0 ;

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

then x * a = b by BINOP_2:def 11;

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