let p be Element of (Polynom-Ring L); :: according to ALGSTR_0:def 16 :: thesis: p is right_complementable
reconsider p1 = p as Polynomial of L by Def12;
reconsider q = - p1 as Element of (Polynom-Ring L) by Def12;
take q ; :: according to ALGSTR_0:def 11 :: thesis: p + q = 0. (Polynom-Ring L)
thus p + q = p1 - p1 by Def12
.= 0_. L by Th30
.= 0. (Polynom-Ring L) by Def12 ; :: thesis: verum