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

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

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

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

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

.= q * aa by BINOP_2:def 11 ;

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

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

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

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

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

.= q * aa by BINOP_2:def 11 ;

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