let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of L

for pc being Element of (Polynom-Ring L) st p = pc holds

- p = - pc

let p be Polynomial of L; :: thesis: for pc being Element of (Polynom-Ring L) st p = pc holds

- p = - pc

let pc be Element of (Polynom-Ring L); :: thesis: ( p = pc implies - p = - pc )

assume A1: p = pc ; :: thesis: - p = - pc

set PRL = Polynom-Ring L;

reconsider mpc = - p as Element of (Polynom-Ring L) by POLYNOM3:def 10;

p + (- p) = p - p

.= 0_. L by POLYNOM3:29 ;

then pc + mpc = 0_. L by A1, POLYNOM3:def 10

.= 0. (Polynom-Ring L) by POLYNOM3:def 10 ;

hence - p = - pc by RLVECT_1:def 10; :: thesis: verum

for pc being Element of (Polynom-Ring L) st p = pc holds

- p = - pc

let p be Polynomial of L; :: thesis: for pc being Element of (Polynom-Ring L) st p = pc holds

- p = - pc

let pc be Element of (Polynom-Ring L); :: thesis: ( p = pc implies - p = - pc )

assume A1: p = pc ; :: thesis: - p = - pc

set PRL = Polynom-Ring L;

reconsider mpc = - p as Element of (Polynom-Ring L) by POLYNOM3:def 10;

p + (- p) = p - p

.= 0_. L by POLYNOM3:29 ;

then pc + mpc = 0_. L by A1, POLYNOM3:def 10

.= 0. (Polynom-Ring L) by POLYNOM3:def 10 ;

hence - p = - pc by RLVECT_1:def 10; :: thesis: verum