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