let p be Element of (Formal-Series (n,L)); :: according to RLVECT_1:def 4 :: thesis: p + (0. (Formal-Series (n,L))) = p
reconsider p1 = p as Series of n,L by Def3;
0. (Formal-Series (n,L)) = 0_ (n,L) by Def3;
hence p + (0. (Formal-Series (n,L))) = p1 + (0_ (n,L)) by Def3
.= p by POLYNOM1:23 ;
:: thesis: verum