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