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

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