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

per cases ( p9 = 0_ (n,L) or p9 <> 0_ (n,L) ) ;

suppose A1: p9 = 0_ (n,L) ; :: thesis: HM (p9,T) <= p9,T

now :: thesis: not Support (HM (p9,T)) <> {}

assume Support (HM (p9,T)) <> {} ; :: thesis: contradiction
then consider u being bag of n such that
A2: Support (HM (p9,T)) = {u} by POLYNOM7:6;
A3: u in Support (HM (p9,T)) by A2, TARSKI:def 1;

now :: thesis: for v being bag of n st v in Support (HM (p9,T)) holds
v <= u,T

let v be bag of n; :: thesis: ( v in Support (HM (p9,T)) implies v <= u,T )
assume v in Support (HM (p9,T)) ; :: thesis: v <= u,T
then u = v by A2, TARSKI:def 1;
hence v <= u,T by TERMORD:6; :: thesis: verum

end;

then A4: HT ((HM (p9,T)),T) = u by A3, TERMORD:def 6;
0. L = p9 . (HT (p9,T)) by A1, POLYNOM1:22
.= HC (p9,T) by TERMORD:def 7
.= HC ((HM (p9,T)),T) by TERMORD:27
.= (HM (p9,T)) . u by A4, TERMORD:def 7 ;
hence contradiction by A3, POLYNOM1:def 4; :: thesis: verum

end;

then HM (p9,T) = 0_ (n,L) by POLYNOM7:1;
hence HM (p9,T) <= p9,T by A1, Th25; :: thesis: verum

end;

suppose p9 <> 0_ (n,L) ; :: thesis: HM (p9,T) <= p9,T

then reconsider p = p9 as non-zero Polynomial of n,L by POLYNOM7:def 1;
set hmp = HM (p,T);
set R = RelStr(# (Bags n),T #);
set x = Support ((HM (p,T)),T);
set y = Support (p,T);
A5: ( (Support ((HM (p,T)),T)) \ {(PosetMax (Support ((HM (p,T)),T)))} is Element of Fin the carrier of RelStr(# (Bags n),T #) & (Support (p,T)) \ {(PosetMax (Support (p,T)))} is Element of Fin the carrier of RelStr(# (Bags n),T #) ) by BAGORDER:37;
A6: PosetMax (Support ((HM (p,T)),T)) = HT ((HM (p,T)),T) by Th24
.= HT (p,T) by TERMORD:26 ;
p <> 0_ (n,L) by POLYNOM7:def 1;
then A7: Support p <> {} by POLYNOM7:1;
(HM (p,T)) . (HT (p,T)) = p . (HT (p,T)) by TERMORD:18
.= HC (p,T) by TERMORD:def 7 ;
then A8: (HM (p,T)) . (HT (p,T)) <> 0. L ;
then A9: Support ((HM (p,T)),T) <> {} by POLYNOM1:def 4;
HT (p,T) in Support (HM (p,T)) by A8, POLYNOM1:def 4;
then Support (HM (p,T)) = {(HT (p,T))} by TERMORD:21;
then (Support ((HM (p,T)),T)) \ {(PosetMax (Support ((HM (p,T)),T)))} = {} by A6, XBOOLE_1:37;
then A10: [((Support ((HM (p,T)),T)) \ {(PosetMax (Support ((HM (p,T)),T)))}),((Support (p,T)) \ {(PosetMax (Support (p,T)))})] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A5, BAGORDER:35;
PosetMax (Support ((HM (p,T)),T)) = PosetMax (Support (p,T)) by A6, Th24;
then [(Support ((HM (p,T)),T)),(Support (p,T))] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A7, A9, A10, BAGORDER:35;
then [(Support ((HM (p,T)),T)),(Support (p,T))] in FinOrd RelStr(# (Bags n),T #) by BAGORDER:def 15;
hence HM (p9,T) <= p9,T ; :: thesis: verum

end;

end;