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