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