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