let p be Element of (Polynom-Ring L); :: according to RLVECT_1:def 4 :: thesis: p + (0. (Polynom-Ring L)) = p

reconsider p1 = p as sequence of L by Def10;

0. (Polynom-Ring L) = 0_. L by Def10;

hence p + (0. (Polynom-Ring L)) = p1 + (0_. L) by Def10

.= p by Th26 ;

:: thesis: verum

reconsider p1 = p as sequence of L by Def10;

0. (Polynom-Ring L) = 0_. L by Def10;

hence p + (0. (Polynom-Ring L)) = p1 + (0_. L) by Def10

.= p by Th26 ;

:: thesis: verum