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 HC (p *' q),T = (HC p,T) * (HC 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 HC (p *' q),O = (HC p,O) * (HC 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 HC (p *' q),O = (HC p,O) * (HC q,O)
let p, q be non-zero Polynomial of n,L; :: thesis: HC (p *' q),O = (HC p,O) * (HC q,O)
thus HC (p *' q),O = (p *' q) . ((HT p,O) + (HT q,O)) by Th31
.= (HC p,O) * (HC q,O) by Lm14 ; :: thesis: verum