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 Def10;

reconsider q = - p1 as Element of (Polynom-Ring L) by Def10;

take q ; :: according to ALGSTR_0:def 11 :: thesis: p + q = 0. (Polynom-Ring L)

thus p + q = p1 - p1 by Def10

.= 0_. L by Th27

.= 0. (Polynom-Ring L) by Def10 ; :: thesis: verum

reconsider p1 = p as Polynomial of L by Def10;

reconsider q = - p1 as Element of (Polynom-Ring L) by Def10;

take q ; :: according to ALGSTR_0:def 11 :: thesis: p + q = 0. (Polynom-Ring L)

thus p + q = p1 - p1 by Def10

.= 0_. L by Th27

.= 0. (Polynom-Ring L) by Def10 ; :: thesis: verum