let n be Ordinal; :: thesis: for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 )
set R = Polynom-Ring (n,L);
reconsider x = - p as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider x = x as Element of (Polynom-Ring (n,L)) ;
assume p = q ; :: thesis: - p = - q
then x + q = (- p) + p by POLYNOM1:def 11
.= 0_ (n,L) by Th3
.= 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11 ;
hence - p = - q by RLVECT_1:6; :: thesis: verum