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