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 7
.= (p . b) + ((- (HM (p,O))) . b) by POLYNOM1:15
.= (p . b) + (- ((HM (p,O)) . b)) by POLYNOM1:17
.= (p . b) + (- (0. L)) by A2, Th19
.= (p . b) + (0. L) by RLVECT_1:12
.= p . b by RLVECT_1:4 ;
then ( b is Element of Bags n & (Red (p,O)) . b <> 0. L ) by A1, POLYNOM1:def 4;
hence b in Support (Red (p,O)) by POLYNOM1:def 4; :: thesis: verum