let x be Element of (Polynom-Ring L); :: according to VECTSP_1:def 6 :: thesis: ( x * (1. (Polynom-Ring L)) = x & (1. (Polynom-Ring L)) * x = x )
thus ( x * (1. (Polynom-Ring L)) = x & (1. (Polynom-Ring L)) * x = x ) by Lm2; :: thesis: verum