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
for b being bag of st b in Support p & b <> HT p,O holds
b 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
for b being bag of st b in Support p & b <> HT p,O holds
b 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
for b being bag of st b in Support p & b <> HT p,O holds
b in Support (Red p,O)
let p be Polynomial of n,L; :: thesis: for b being bag of st b in Support p & b <> HT p,O holds
b in Support (Red p,O)
let b be bag of ; :: thesis: ( b in Support p & b <> HT p,O implies b in Support (Red p,O) )
assume A1: ( b in Support p & b <> HT p,O ) ; :: thesis: b in Support (Red p,O)
A2: b is Element of Bags n by POLYNOM1:def 14;
(Red p,O) . b = (p + (- (HM p,O))) . b by POLYNOM1:def 23
.= (p . b) + ((- (HM p,O)) . b) by POLYNOM1:def 21
.= (p . b) + (- ((HM p,O) . b)) by POLYNOM1:def 22
.= (p . b) + (- (0. L)) by A1, Th19
.= (p . b) + (0. L) by RLVECT_1:25
.= p . b by RLVECT_1:10 ;
then (Red p,O) . b <> 0. L by A1, POLYNOM1:def 9;
hence b in Support (Red p,O) by A2, POLYNOM1:def 9; :: thesis: verum