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