let a, x, y be Element of multEX_0; ( a <> 0. multEX_0 & x * a = y * a implies x = y )
assume A1:
a <> 0. multEX_0
; ( not x * a = y * a or x = y )
reconsider aa = a, p = x, q = y as Real ;
assume
x * a = y * a
; 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; verum