let n be Ordinal; :: thesis: for L being non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L
for q being Element of (Polynom-Ring n,L) st p = q holds
- p = - q
let L be non trivial right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for q being Element of (Polynom-Ring n,L) st p = q holds
- p = - q
let p be Polynomial of n,L; :: thesis: for q being Element of (Polynom-Ring n,L) st p = q holds
- p = - q
let q be Element of (Polynom-Ring n,L); :: thesis: ( p = q implies - p = - q )
assume A1: p = q ; :: thesis: - p = - q
set R = Polynom-Ring n,L;
reconsider x = - p as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider x = x as Element of (Polynom-Ring n,L) ;
x + q = (- p) + p by A1, POLYNOM1:def 27
.= 0_ n,L by Th3
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;
hence - p = - q by RLVECT_1:19; :: thesis: verum