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)
set b = (HT (p,O)) + (HT (q,O));
assume A1: not (HT (p,O)) + (HT (q,O)) in Support (p *' q) ; :: thesis: contradiction
p <> 0_ (n,L) by POLYNOM7:def 1;
then Support p <> {} by POLYNOM7:1;
then HT (p,O) in Support p by Def6;
then A2: p . (HT (p,O)) <> 0. L by POLYNOM1:def 4;
q <> 0_ (n,L) by POLYNOM7:def 1;
then Support q <> {} by POLYNOM7:1;
then HT (q,O) in Support q by Def6;
then A3: q . (HT (q,O)) <> 0. L by POLYNOM1:def 4;
(HT (p,O)) + (HT (q,O)) is Element of Bags n by PRE_POLY:def 12;
then (p *' q) . ((HT (p,O)) + (HT (q,O))) = 0. L by A1, POLYNOM1:def 4;
then (p . (HT (p,O))) * (q . (HT (q,O))) = 0. L by Lm14;
hence contradiction by A2, A3, VECTSP_2:def 1; :: thesis: verum