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 )
assume A1: f = p ; :: thesis: - f = - p
reconsider x = - p as Element of (Polynom-Ring L) by POLYNOM3:def 12;
reconsider x = x as Element of (Polynom-Ring L) ;
f + x = p - p by A1, POLYNOM3:def 12
.= 0_. L by POLYNOM3:30
.= 0. (Polynom-Ring L) by POLYNOM3:def 12 ;
then f = - x by RLVECT_1:19;
hence - f = - p by RLVECT_1:30; :: thesis: verum