let p be Element of (Formal-Series L); :: according to ALGSTR_0:def 16 :: thesis: p is right_complementable
reconsider p1 = p as sequence of L by Def2;
reconsider q = - p1 as Element of (Formal-Series L) by Def2;
take q ; :: according to ALGSTR_0:def 11 :: thesis: p + q = 0. (Formal-Series L)
thus p + q = p1 + (- p1) by Def2
.= p1 - p1 by POLYNOM3:def 6
.= 0_. L by POLYNOM3:29
.= 0. (Formal-Series L) by Def2 ; :: thesis: verum