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 4; :: thesis: verum