let v be Element of (Polynom-Ring (n,L)); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider p = v as Polynomial of n,L by Def11;
reconsider w = - p as Element of (Polynom-Ring (n,L)) by Def11;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. (Polynom-Ring (n,L))
thus v + w = p - p by Def11
.= 0_ (n,L) by Th24
.= 0. (Polynom-Ring (n,L)) by Def11 ; :: thesis: verum