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