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;
A1: a <> 0. L by STRUCT_0:def 12;

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

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

now

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

end;

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

end;

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

now

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

end;

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

A7: now

let b be bag of n; :: thesis: ( b in Support (a * p) implies b <= HT p,T,T )
assume A8: 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 A8, TERMORD:def 6; :: thesis: verum

end;

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

end;

end;