let n be Ordinal; :: thesis: for O being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O))
let O be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O))
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L holds not HT (p,O) in Support (Red (p,O))
let p be Polynomial of n,L; :: thesis: not HT (p,O) in Support (Red (p,O))
assume HT (p,O) in Support (Red (p,O)) ; :: thesis: contradiction
then (Red (p,O)) . (HT (p,O)) <> 0. L by POLYNOM1:def 4;
then (p + (- (HM (p,O)))) . (HT (p,O)) <> 0. L by POLYNOM1:def 7;
then (p . (HT (p,O))) + ((- (HM (p,O))) . (HT (p,O))) <> 0. L by POLYNOM1:15;
then A1: (p . (HT (p,O))) + (- ((HM (p,O)) . (HT (p,O)))) <> 0. L by POLYNOM1:17;
(HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) by Lm8;
hence contradiction by A1, RLVECT_1:def 10; :: thesis: verum