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 <> HT (p,O) holds
(Red (p,O)) . b = p . b
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 <> HT (p,O) holds
(Red (p,O)) . b = p . b
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 <> HT (p,O) holds
(Red (p,O)) . b = p . b
let p be Polynomial of n,L; :: thesis: for b being bag of n st b <> HT (p,O) holds
(Red (p,O)) . b = p . b
let b be bag of n; :: thesis: ( b <> HT (p,O) implies (Red (p,O)) . b = p . b )
A1: b is Element of Bags n by PRE_POLY:def 12;
assume b <> HT (p,O) ; :: thesis: (Red (p,O)) . b = p . b
then not b in {(HT (p,O))} by TARSKI:def 1;
then A2: not b in Support (HM (p,O)) by Lm12;
thus (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, A1, POLYNOM1:def 4
.= (p . b) + (0. L) by RLVECT_1:12
.= p . b by RLVECT_1:4 ; :: thesis: verum