let a be Element of multEX_0; :: thesis: a * (0. multEX_0) = 0. multEX_0
reconsider aa = a as Real ;
thus a * (0. multEX_0) = aa * 0 by BINOP_2:def 11
.= 0. multEX_0 ; :: thesis: verum