let n be Ordinal; :: thesis: for T 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 (Red p,T) . (HT p,T) = 0. L
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 (Red p,O) . (HT p,O) = 0. L
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L holds (Red p,O) . (HT p,O) = 0. L
let p be Polynomial of n,L; :: thesis: (Red p,O) . (HT p,O) = 0. L
( HT p,O in {(HT p,O)} & Support (Red p,O) = (Support p) \ {(HT p,O)} ) by Lm17, TARSKI:def 1;
then not HT p,O in Support (Red p,O) by XBOOLE_0:def 5;
hence (Red p,O) . (HT p,O) = 0. L by POLYNOM1:def 9; :: thesis: verum