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 15;

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 u' = u as Element of Bags n ;
A3: p . u' <> 0. L by POLYNOM1:def 9;
A4: a <> 0. L by STRUCT_0:def 15;
(a * p) . u' = a * (p . u') by POLYNOM7:def 10;
then (a * p) . u' <> 0. L by A3, A4, 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 A5: Support (a * p) <> {} ; :: thesis: HT (a * p),T = HT p,T

now

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

end;

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

now

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

end;

hence HT (a * p),T = HT p,T by A9, TERMORD:def 6; :: thesis: verum

end;

end;