let R be Ring; :: thesis: for a being Element of (Polynom-Ring R)
for b being Polynomial of R st a = b holds
- a = - b
let a be Element of (Polynom-Ring R); :: thesis: for b being Polynomial of R st a = b holds
- a = - b
let b be Polynomial of R; :: thesis: ( a = b implies - a = - b )
assume AS: a = b ; :: thesis: - a = - b
set K = Polynom-Ring R;
reconsider c = - b as Element of (Polynom-Ring R) by POLYNOM3:def 10;
a + c = b - b by AS, POLYNOM3:def 10
.= 0_. R by POLYNOM3:29
.= 0. (Polynom-Ring R) by POLYNOM3:def 10
.= a + (- a) by RLVECT_1:5 ;
hence - a = - b by RLVECT_1:8; :: thesis: verum