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 Def27;
reconsider w = - p as Element of (Polynom-Ring n,L) by Def27;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. (Polynom-Ring n,L)
thus v + w = p - p by Def27
.= 0_ n,L by Th83
.= 0. (Polynom-Ring n,L) by Def27 ; :: thesis: verum