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 9;
then (p + (- (HM p,O))) . (HT p,O) <> 0. L by POLYNOM1:def 23;
then (p . (HT p,O)) + ((- (HM p,O)) . (HT p,O)) <> 0. L by POLYNOM1:def 21;
then A1: (p . (HT p,O)) + (- ((HM p,O) . (HT p,O))) <> 0. L by POLYNOM1:def 22;
(HM p,O) . (HT p,O) = p . (HT p,O) by Lm8;
hence contradiction by A1, RLVECT_1:def 13; :: thesis: verum