let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of L
for f being Element of (Polynom-Ring L) st f = p holds
- f = - p
let p be Polynomial of L; :: thesis: for f being Element of (Polynom-Ring L) st f = p holds
- f = - p
let f be Element of (Polynom-Ring L); :: thesis: ( f = p implies - f = - p )
reconsider x = - p as Element of (Polynom-Ring L) by POLYNOM3:def 10;
reconsider x = x as Element of (Polynom-Ring L) ;
assume f = p ; :: thesis: - f = - p
then f + x = p - p by POLYNOM3:def 10
.= 0_. L by POLYNOM3:29
.= 0. (Polynom-Ring L) by POLYNOM3:def 10 ;
then f = - x by RLVECT_1:6;
hence - f = - p by RLVECT_1:17; :: thesis: verum