let x be Element of multEX_0; :: according to VECTSP_1:def 6 :: thesis: ( x * (1. multEX_0) = x & (1. multEX_0) * x = x )
thus ( x * (1. multEX_0) = x & (1. multEX_0) * x = x ) by Lm15; :: thesis: verum