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