let p be Element of (Polynom-Ring L); :: according to RLVECT_1:def 7 :: thesis: p + (0. (Polynom-Ring L)) = p
reconsider p1 = p as sequence of L by Def12;
0. (Polynom-Ring L) = 0_. L by Def12;
hence p + (0. (Polynom-Ring L)) = p1 + (0_. L) by Def12
.= p by Th29 ;
:: thesis: verum