let p be Element of (Formal-Series (n,L)); :: according to ALGSTR_0:def 16 :: thesis: p is right_complementable
reconsider p1 = p as Series of n,L by Def3;
reconsider q = - p1 as Element of (Formal-Series (n,L)) by Def3;
take q ; :: according to ALGSTR_0:def 11 :: thesis: p + q = 0. (Formal-Series (n,L))
thus p + q = p1 - p1 by Def3
.= 0_ (n,L) by POLYNOM1:24
.= 0. (Formal-Series (n,L)) by Def3 ; :: thesis: verum