let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)
let T be connected TermOrder of n; :: thesis: for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)
let p be Polynomial of n,L; :: thesis: HT ((- p),T) = HT (p,T)

per cases ( p = 0_ (n,L) or p <> 0_ (n,L) ) ;

suppose A1: p = 0_ (n,L) ; :: thesis: HT ((- p),T) = HT (p,T)

reconsider x = - p as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider x = x as Element of (Polynom-Ring (n,L)) ;
A2: - (0_ (n,L)) = (- (0_ (n,L))) + (0_ (n,L)) by POLYNOM1:23
.= 0_ (n,L) by POLYRED:3 ;
0. (Polynom-Ring (n,L)) = 0_ (n,L) by POLYNOM1:def 11;
then x + (0. (Polynom-Ring (n,L))) = (- p) + (0_ (n,L)) by POLYNOM1:def 11
.= 0_ (n,L) by A1, A2, POLYNOM1:23
.= 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11 ;
then - p = - (0. (Polynom-Ring (n,L))) by RLVECT_1:6
.= 0. (Polynom-Ring (n,L)) by RLVECT_1:12
.= p by A1, POLYNOM1:def 11 ;
hence HT ((- p),T) = HT (p,T) ; :: thesis: verum

end;

suppose p <> 0_ (n,L) ; :: thesis: HT ((- p),T) = HT (p,T)

then A3: Support p <> {} by POLYNOM7:1;
then Support (- p) <> {} by Th5;
then HT ((- p),T) in Support (- p) by TERMORD:def 6;
then HT ((- p),T) in Support p by Th5;
then A4: HT ((- p),T) <= HT (p,T),T by TERMORD:def 6;
HT (p,T) in Support p by A3, TERMORD:def 6;
then HT (p,T) in Support (- p) by Th5;
then HT (p,T) <= HT ((- p),T),T by TERMORD:def 6;
hence HT ((- p),T) = HT (p,T) by A4, TERMORD:7; :: thesis: verum

end;

end;