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 holds Support (Red (p,O)) = (Support p) \ {(HT (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 holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L holds Support (Red (p,O)) = (Support p) \ {(HT (p,O))}
let p be Polynomial of n,L; :: thesis: Support (Red (p,O)) = (Support p) \ {(HT (p,O))}

A1: now :: thesis: for u being object st u in Support (Red (p,O)) holds
u in (Support p) \ {(HT (p,O))}

let u be object ; :: thesis: ( u in Support (Red (p,O)) implies u in (Support p) \ {(HT (p,O))} )
assume A2: u in Support (Red (p,O)) ; :: thesis: u in (Support p) \ {(HT (p,O))}
then reconsider u9 = u as Element of Bags n ;
reconsider u9 = u9 as bag of n ;
A3: (p - (HM (p,O))) . u9 <> 0. L by A2, POLYNOM1:def 4;
A4: not u9 = HT (p,O) by A2, Lm15;
(p + (- (HM (p,O)))) . u9 = (p . u9) + ((- (HM (p,O))) . u9) by POLYNOM1:15
.= (p . u9) + (- ((HM (p,O)) . u9)) by POLYNOM1:17 ;
then (p + (- (HM (p,O)))) . u9 = (p . u9) + (- (0. L)) by A4, Th19
.= (p . u9) + (0. L) by RLVECT_1:12
.= p . u9 by RLVECT_1:4 ;
then p . u9 <> 0. L by A3, POLYNOM1:def 7;
then A5: u9 in Support p by POLYNOM1:def 4;
not u9 in {(HT (p,O))} by A4, TARSKI:def 1;
hence u in (Support p) \ {(HT (p,O))} by A5, XBOOLE_0:def 5; :: thesis: verum

end;

now :: thesis: for u being object st u in (Support p) \ {(HT (p,O))} holds
u in Support (Red (p,O))

let u be object ; :: thesis: ( u in (Support p) \ {(HT (p,O))} implies u in Support (Red (p,O)) )
assume A6: u in (Support p) \ {(HT (p,O))} ; :: thesis: u in Support (Red (p,O))
then reconsider u9 = u as Element of Bags n ;
reconsider u9 = u9 as bag of n ;
not u in {(HT (p,O))} by A6, XBOOLE_0:def 5;
then A7: u9 <> HT (p,O) by TARSKI:def 1;
u in Support p by A6, XBOOLE_0:def 5;
hence u in Support (Red (p,O)) by A7, Lm16; :: thesis: verum

end;

hence Support (Red (p,O)) = (Support p) \ {(HT (p,O))} by A1, TARSKI:2; :: thesis: verum