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

A1: now

let u be set ; :: thesis: ( u in Support p implies u in Support ((HM p,O) + (Red p,O)) )
assume A2: u in Support p ; :: thesis: u in Support ((HM p,O) + (Red p,O))
then reconsider u' = u as Element of Bags n ;
reconsider u' = u' as bag of ;
A3: p . u' <> 0. L by A2, POLYNOM1:def 9;

now

per cases ( u' = HT p,O or u' <> HT p,O ) ;

case A4: u' = HT p,O ; :: thesis: u' in Support ((HM p,O) + (Red p,O))

then A5: p . (HT p,O) <> 0. L by A2, POLYNOM1:def 9;
((HM p,O) + (Red p,O)) . u' = ((HM p,O) . u') + ((Red p,O) . u') by POLYNOM1:def 21
.= ((HM p,O) . u') + (0. L) by A4, Lm18
.= (HM p,O) . u' by RLVECT_1:10
.= HC p,O by A4, Lm8 ;
hence u' in Support ((HM p,O) + (Red p,O)) by A5, POLYNOM1:def 9; :: thesis: verum

end;

case A6: u' <> HT p,O ; :: thesis: u' in Support ((HM p,O) + (Red p,O))

((HM p,O) + (Red p,O)) . u' = ((HM p,O) . u') + ((Red p,O) . u') by POLYNOM1:def 21
.= ((HM p,O) . u') + (p . u') by A6, Lm19
.= (0. L) + (p . u') by A6, Th19
.= p . u' by RLVECT_1:10 ;
hence u' in Support ((HM p,O) + (Red p,O)) by A3, POLYNOM1:def 9; :: thesis: verum

end;

end;

end;

hence u in Support ((HM p,O) + (Red p,O)) ; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in Support ((HM p,O) + (Red p,O)) implies u in Support p )
assume A7: u in Support ((HM p,O) + (Red p,O)) ; :: thesis: u in Support p
then reconsider u' = u as Element of Bags n ;
reconsider u' = u' as bag of ;
A8: ((HM p,O) + (Red p,O)) . u' <> 0. L by A7, POLYNOM1:def 9;

now

per cases ( u' = HT p,O or u' <> HT p,O ) ;

case A9: u' = HT p,O ; :: thesis: u' in Support p

((HM p,O) + (Red p,O)) . u' = ((HM p,O) . u') + ((Red p,O) . u') by POLYNOM1:def 21
.= ((HM p,O) . (HT p,O)) + (0. L) by A9, Lm18
.= (HM p,O) . (HT p,O) by RLVECT_1:10
.= p . u' by A9, Lm8 ;
hence u' in Support p by A8, POLYNOM1:def 9; :: thesis: verum

end;

case A10: u' <> HT p,O ; :: thesis: u' in Support p

((HM p,O) + (Red p,O)) . u' = ((HM p,O) . u') + ((Red p,O) . u') by POLYNOM1:def 21
.= (0. L) + ((Red p,O) . u') by A10, Th19
.= (Red p,O) . u' by RLVECT_1:10
.= p . u by A10, Lm19 ;
hence u' in Support p by A8, POLYNOM1:def 9; :: thesis: verum

end;

end;

end;

hence u in Support p ; :: thesis: verum

end;

hence Support ((HM p,O) + (Red p,O)) = Support p by A1, TARSKI:2; :: thesis: verum