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

let u be set ; :: 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 u' = u as Element of Bags n ;
reconsider u' = u' as bag of n ;
A3: (p - (HM p,O)) . u' <> 0. L by A2, POLYNOM1:def 9;
A4: not u' = HT p,O by A2, Lm15;
(p + (- (HM p,O))) . u' = (p . u') + ((- (HM p,O)) . u') by POLYNOM1:def 21
.= (p . u') + (- ((HM p,O) . u')) by POLYNOM1:def 22 ;
then (p + (- (HM p,O))) . u' = (p . u') + (- (0. L)) by A4, Th19
.= (p . u') + (0. L) by RLVECT_1:25
.= p . u' by RLVECT_1:10 ;
then p . u' <> 0. L by A3, POLYNOM1:def 23;
then A5: u' in Support p by POLYNOM1:def 9;
not u' 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

let u be set ; :: 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 u' = u as Element of Bags n ;
reconsider u' = u' as bag of n ;
not u in {(HT p,O)} by A6, XBOOLE_0:def 5;
then A7: u' <> 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