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