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)
A1: (HT p,O) + (HT q,O) is Element of Bags n by PRE_POLY:def 12;
(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) <> {} by Th29;
then A3: HT (p *' q),O in Support (p *' q) by Def6;
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 A3;
then consider s, t being Element of Bags n such that
A4: HT (p *' q),O = s + t and
A5: s in Support p and
A6: t in Support q ;
s <= HT p,O,O by A5, Def6;
then [s,(HT p,O)] in O by Def2;
then A7: [(s + t),((HT p,O) + t)] in O by BAGORDER:def 7;
t <= HT q,O,O by A6, Def6;
then [t,(HT q,O)] in O by Def2;
then A8: [(t + (HT p,O)),((HT p,O) + (HT q,O))] in O by BAGORDER:def 7;
( s + t is Element of Bags n & (HT p,O) + t is Element of Bags n ) by PRE_POLY:def 12;
then [(s + t),((HT p,O) + (HT q,O))] in O by A1, A7, A8, ORDERS_1:14;
hence HT (p *' q),O = (HT p,O) + (HT q,O) by A2, A4, A1, ORDERS_1:13; :: thesis: verum