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