let L be Ring; :: thesis: for a being Element of (Polynom-Ring L)

for p being Polynomial of L st a = p holds

- a = - p

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

- a = - p

let p be Polynomial of L; :: thesis: ( a = p implies - a = - p )

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

assume a = p ; :: thesis: - a = - p

then a + x = p + (- p) by POLYNOM3:def 10

.= p - p by POLYNOM3:def 6

.= 0_. L by POLYNOM3:29

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

then a = - x by RLVECT_1:6;

hence - a = - p ; :: thesis: verum

for p being Polynomial of L st a = p holds

- a = - p

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

- a = - p

let p be Polynomial of L; :: thesis: ( a = p implies - a = - p )

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

assume a = p ; :: thesis: - a = - p

then a + x = p + (- p) by POLYNOM3:def 10

.= p - p by POLYNOM3:def 6

.= 0_. L by POLYNOM3:29

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

then a = - x by RLVECT_1:6;

hence - a = - p ; :: thesis: verum