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 :: thesis: for u being object st u in Support p holds
u in Support ((HM (p,O)) + (Red (p,O)))

let u be object ; :: 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 u9 = u as Element of Bags n ;
reconsider u9 = u9 as bag of n ;
A3: p . u9 <> 0. L by A2, POLYNOM1:def 4;

now :: thesis: ( ( u9 = HT (p,O) & u9 in Support ((HM (p,O)) + (Red (p,O))) ) or ( u9 <> HT (p,O) & u9 in Support ((HM (p,O)) + (Red (p,O))) ) )

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

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

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

end;

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

((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15
.= ((HM (p,O)) . u9) + (p . u9) by A6, Lm19
.= (0. L) + (p . u9) by A6, Th19
.= p . u9 by RLVECT_1:4 ;
hence u9 in Support ((HM (p,O)) + (Red (p,O))) by A3, POLYNOM1:def 4; :: thesis: verum

end;

end;

end;

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

end;

now :: thesis: for u being object st u in Support ((HM (p,O)) + (Red (p,O))) holds
u in Support p

let u be object ; :: 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 u9 = u as Element of Bags n ;
reconsider u9 = u9 as bag of n ;
A8: ((HM (p,O)) + (Red (p,O))) . u9 <> 0. L by A7, POLYNOM1:def 4;

now :: thesis: ( ( u9 = HT (p,O) & u9 in Support p ) or ( u9 <> HT (p,O) & u9 in Support p ) )

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

case A9: u9 = HT (p,O) ; :: thesis: u9 in Support p

((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15
.= ((HM (p,O)) . (HT (p,O))) + (0. L) by A9, Lm18
.= (HM (p,O)) . (HT (p,O)) by RLVECT_1:4
.= p . u9 by A9, Lm8 ;
hence u9 in Support p by A8, POLYNOM1:def 4; :: thesis: verum

end;

case A10: u9 <> HT (p,O) ; :: thesis: u9 in Support p

((HM (p,O)) + (Red (p,O))) . u9 = ((HM (p,O)) . u9) + ((Red (p,O)) . u9) by POLYNOM1:15
.= (0. L) + ((Red (p,O)) . u9) by A10, Th19
.= (Red (p,O)) . u9 by RLVECT_1:4
.= p . u by A10, Lm19 ;
hence u9 in Support p by A8, POLYNOM1:def 4; :: 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