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 p) \ {(HT p,O)} implies u in Support (Red p,O) )
assume A2: u in (Support p) \ {(HT p,O)} ; :: thesis: u in Support (Red p,O)
then A3: ( u in Support p & not u in {(HT p,O)} ) by XBOOLE_0:def 5;
reconsider u' = u as Element of Bags n by A2;
reconsider u' = u' as bag of ;
u' <> HT p,O by A3, TARSKI:def 1;
hence u in Support (Red p,O) by A3, Lm16; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in Support (Red p,O) implies u in (Support p) \ {(HT p,O)} )
assume A4: 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 ;
A5: (p - (HM p,O)) . u' <> 0. L by A4, POLYNOM1:def 9;
A6: (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 ;
A7: not u' = HT p,O by A4, Lm15;
then (p + (- (HM p,O))) . u' = (p . u') + (- (0. L)) by A6, Th19
.= (p . u') + (0. L) by RLVECT_1:25
.= p . u' by RLVECT_1:10 ;
then p . u' <> 0. L by A5, POLYNOM1:def 23;
then A8: u' in Support p by POLYNOM1:def 9;
not u' in {(HT p,O)} by A7, TARSKI:def 1;
hence u in (Support p) \ {(HT p,O)} by A8, XBOOLE_0:def 5; :: thesis: verum

end;

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