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