let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HT (p *' q),T = (HT p,T) + (HT q,T)
let O be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HT (p *' q),O = (HT p,O) + (HT q,O)
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p, q being non-zero Polynomial of n,L holds HT (p *' q),O = (HT p,O) + (HT q,O)
let p, q be non-zero Polynomial of n,L; :: thesis: HT (p *' q),O = (HT p,O) + (HT q,O)
Support (p *' q) <> {} by Th29;
then A1: HT (p *' q),O in Support (p *' q) by Def6;
(HT p,O) + (HT q,O) in Support (p *' q) by Th29;
then (HT p,O) + (HT q,O) <= HT (p *' q),O,O by Def6;
then A2: [((HT p,O) + (HT q,O)),(HT (p *' q),O)] in O by Def2;
Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by Th30;
then HT (p *' q),O in { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) } by A1;
then consider s, t being Element of Bags n such that
A3: ( HT (p *' q),O = s + t & s in Support p & t in Support q ) ;
( s <= HT p,O,O & t <= HT q,O,O ) by A3, Def6;
then A4: ( [s,(HT p,O)] in O & [t,(HT q,O)] in O ) by Def2;
A5: ( s + t is Element of Bags n & (HT p,O) + t is Element of Bags n & HT (p *' q),O is Element of Bags n & (HT p,O) + (HT q,O) is Element of Bags n ) by POLYNOM1:def 14;
A6: [(s + t),((HT p,O) + t)] in O by A4, BAGORDER:def 7;
[(t + (HT p,O)),((HT p,O) + (HT q,O))] in O by A4, BAGORDER:def 7;
then [(s + t),((HT p,O) + (HT q,O))] in O by A5, A6, ORDERS_1:14;
hence HT (p *' q),O = (HT p,O) + (HT q,O) by A2, A3, A5, ORDERS_1:13; :: thesis: verum