let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for a being non zero Element of L holds HT ((a * p),T) = HT (p,T)
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for a being non zero Element of L holds HT ((a * p),T) = HT (p,T)
let L be non trivial right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for a being non zero Element of L holds HT ((a * p),T) = HT (p,T)
let p be Polynomial of n,L; :: thesis: for a being non zero Element of L holds HT ((a * p),T) = HT (p,T)
let a be non zero Element of L; :: thesis: HT ((a * p),T) = HT (p,T)
set ht = HT ((a * p),T);
set htp = HT (p,T);

per cases ( Support (a * p) = {} or Support (a * p) <> {} ) ;

suppose A1: Support (a * p) = {} ; :: thesis: HT ((a * p),T) = HT (p,T)

now :: thesis: not Support p <> {}

assume Support p <> {} ; :: thesis: contradiction
then reconsider sp = Support p as non empty set ;
set u = the Element of sp;
the Element of sp in Support p ;
then reconsider u9 = the Element of sp as Element of Bags n ;
A2: (a * p) . u9 = a * (p . u9) by POLYNOM7:def 9;
( p . u9 <> 0. L & a <> 0. L ) by POLYNOM1:def 4;
then (a * p) . u9 <> 0. L by A2, VECTSP_2:def 1;
hence contradiction by A1, POLYNOM1:def 4; :: thesis: verum

end;

hence HT (p,T) = EmptyBag n by TERMORD:def 6
.= HT ((a * p),T) by A1, TERMORD:def 6 ;
:: thesis: verum

end;

suppose A3: Support (a * p) <> {} ; :: thesis: HT ((a * p),T) = HT (p,T)

now :: thesis: not Support p = {}

reconsider sp = Support (a * p) as non empty set by A3;
set u = the Element of sp;
the Element of sp in Support (a * p) ;
then reconsider u9 = the Element of sp as Element of Bags n ;
( (a * p) . u9 <> 0. L & (a * p) . u9 = a * (p . u9) ) by POLYNOM1:def 4, POLYNOM7:def 9;
then A4: p . u9 <> 0. L ;
assume Support p = {} ; :: thesis: contradiction
hence contradiction by A4, POLYNOM1:def 4; :: thesis: verum

end;

then HT (p,T) in Support p by TERMORD:def 6;
then A5: p . (HT (p,T)) <> 0. L by POLYNOM1:def 4;

A6: now :: thesis: for b being bag of n st b in Support (a * p) holds
b <= HT (p,T),T

let b be bag of n; :: thesis: ( b in Support (a * p) implies b <= HT (p,T),T )
assume A7: b in Support (a * p) ; :: thesis: b <= HT (p,T),T
Support (a * p) c= Support p by Th19;
hence b <= HT (p,T),T by A7, TERMORD:def 6; :: thesis: verum

end;

(a * p) . (HT (p,T)) = a * (p . (HT (p,T))) by POLYNOM7:def 9;
then (a * p) . (HT (p,T)) <> 0. L by A5, VECTSP_2:def 1;
then HT (p,T) in Support (a * p) by POLYNOM1:def 4;
hence HT ((a * p),T) = HT (p,T) by A6, TERMORD:def 6; :: thesis: verum

end;

end;