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 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, A1, POLYNOM1:def 9
.= (p . b) + (0. L) by RLVECT_1:25
.= p . b by RLVECT_1:10 ; :: thesis: verum