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