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 left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (HT p,T) + (HT q,T) in Support (p *' q)
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 left_zeroed doubleLoopStr
for p, q being non-zero Polynomial of n,L holds (HT p,O) + (HT q,O) in Support (p *' q)
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like left_zeroed doubleLoopStr ; :: thesis: for p, q being non-zero Polynomial of n,L holds (HT p,O) + (HT q,O) in Support (p *' q)
let p, q be non-zero Polynomial of n,L; :: thesis: (HT p,O) + (HT q,O) in Support (p *' q)
( p <> 0_ n,L & q <> 0_ n,L ) by POLYNOM7:def 2;
then ( Support p <> {} & Support q <> {} ) by POLYNOM7:1;
then ( HT p,O in Support p & HT q,O in Support q ) by Def6;
then A1: ( p . (HT p,O) <> 0. L & q . (HT q,O) <> 0. L ) by POLYNOM1:def 9;
set b = (HT p,O) + (HT q,O);
A2: (HT p,O) + (HT q,O) is Element of Bags n by POLYNOM1:def 14;
assume not (HT p,O) + (HT q,O) in Support (p *' q) ; :: thesis: contradiction
then (p *' q) . ((HT p,O) + (HT q,O)) = 0. L by A2, POLYNOM1:def 9;
then (p . (HT p,O)) * (q . (HT q,O)) = 0. L by Lm14;
hence contradiction by A1, VECTSP_2:def 5; :: thesis: verum