let v be Element of (Polynom-Ring (n,L)); :: according to RLVECT_1:def 4 :: thesis: v + (0. (Polynom-Ring (n,L))) = v
reconsider p = v as Polynomial of n,L by Def11;
0. (Polynom-Ring (n,L)) = 0_ (n,L) by Def11;
hence v + (0. (Polynom-Ring (n,L))) = p + (0_ (n,L)) by Def11
.= v by Th23 ;
:: thesis: verum