let p be Element of (Formal-Series L); :: according to RLVECT_1:def 4 :: thesis: p + (0. (Formal-Series L)) = p
reconsider p1 = p as sequence of L by Def2;
0. (Formal-Series L) = 0_. L by Def2;
hence p + (0. (Formal-Series L)) = p1 + (0_. L) by Def2
.= p by POLYNOM3:28 ;
:: thesis: verum