let R be Ring; :: thesis: for p being Polynomial of R
for q being Element of the carrier of (Polynom-Ring R) st p = q holds
- p = - q
let p be Polynomial of R; :: thesis: for q being Element of the carrier of (Polynom-Ring R) st p = q holds
- p = - q
let q be Element of the carrier of (Polynom-Ring R); :: thesis: ( p = q implies - p = - q )
assume AS: p = q ; :: thesis: - p = - q
reconsider r = - p as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;

now :: thesis: for n being Element of NAT holds (p + (- p)) . n = (0_. R) . n

let n be Element of NAT ; :: thesis: (p + (- p)) . n = (0_. R) . n
thus (p + (- p)) . n = (p . n) + ((- p) . n) by NORMSP_1:def 2
.= (p . n) + (- (p . n)) by BHSP_1:44
.= (0_. R) . n by RLVECT_1:5 ; :: thesis: verum

end;

then p + (- p) = 0_. R ;
then q + r = 0_. R by AS, POLYNOM3:def 10;
then q + r = 0. (Polynom-Ring R) by POLYNOM3:def 10;
hence - p = - q by RLVECT_1:6; :: thesis: verum