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