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 27;
reconsider x = x as Element of (Polynom-Ring n,L) ;
A2: - (0_ n,L) = (- (0_ n,L)) + (0_ n,L) by POLYNOM1:82
.= 0_ n,L by POLYRED:3 ;
0. (Polynom-Ring n,L) = 0_ n,L by POLYNOM1:def 27;
then x + (0. (Polynom-Ring n,L)) = (- p) + (0_ n,L) by POLYNOM1:def 27
.= 0_ n,L by A1, A2, POLYNOM1:82
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;
then - p = - (0. (Polynom-Ring n,L)) by RLVECT_1:19
.= 0. (Polynom-Ring n,L) by RLVECT_1:25
.= p by A1, POLYNOM1:def 27 ;
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;