let a, x, y be Element of multEX_0; :: thesis: ( a <> 0. multEX_0 & a * x = a * y implies x = y )

assume A1: a <> 0. multEX_0 ; :: thesis: ( not a * x = a * y or x = y )

reconsider aa = a, p = x, q = y as Real ;

assume a * x = a * y ; :: thesis: x = y

then aa * p = a * y by BINOP_2:def 11

.= aa * q by BINOP_2:def 11 ;

hence x = y by A1, XCMPLX_1:5; :: thesis: verum

assume A1: a <> 0. multEX_0 ; :: thesis: ( not a * x = a * y or x = y )

reconsider aa = a, p = x, q = y as Real ;

assume a * x = a * y ; :: thesis: x = y

then aa * p = a * y by BINOP_2:def 11

.= aa * q by BINOP_2:def 11 ;

hence x = y by A1, XCMPLX_1:5; :: thesis: verum