let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of n,L holds HT ((p + q),T) <= max ((HT (p,T)),(HT (q,T)),T),T
let O be connected admissible TermOrder of n; :: thesis: for L being non empty right_zeroed addLoopStr
for p, q being Polynomial of n,L holds HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
let L be non empty right_zeroed addLoopStr ; :: thesis: for p, q being Polynomial of n,L holds HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O
let p, q be Polynomial of n,L; :: thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O

per cases ( HT ((p + q),O) in Support (p + q) or not HT ((p + q),O) in Support (p + q) ) ;

suppose A1: HT ((p + q),O) in Support (p + q) ; :: thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O

A2: Support (p + q) c= (Support p) \/ (Support q) by POLYNOM1:20;

now :: thesis: ( ( HT ((p + q),O) in Support p & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) or ( HT ((p + q),O) in Support q & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) )

per cases ( HT ((p + q),O) in Support p or HT ((p + q),O) in Support q ) by A1, A2, XBOOLE_0:def 3;

case A3: HT ((p + q),O) in Support p ; :: thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O

then A4: HT ((p + q),O) <= HT (p,O),O by Def6;

now :: thesis: ( ( max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) or ( max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) )

per cases ( max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) or max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) ) by Th12;

case max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) ; :: thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O

hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A3, Def6; :: thesis: verum

end;

case A5: max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) ; :: thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O

then HT (p,O) <= HT (q,O),O by Th14;
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A4, A5, Th8; :: thesis: verum

end;

end;

end;

hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ; :: thesis: verum

end;

case A6: HT ((p + q),O) in Support q ; :: thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O

then A7: HT ((p + q),O) <= HT (q,O),O by Def6;

now :: thesis: ( ( max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) or ( max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) & HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ) )

per cases ( max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) or max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) ) by Th12;

case max ((HT (p,O)),(HT (q,O)),O) = HT (q,O) ; :: thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O

hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A6, Def6; :: thesis: verum

end;

case A8: max ((HT (p,O)),(HT (q,O)),O) = HT (p,O) ; :: thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O

then HT (q,O) <= HT (p,O),O by Th14;
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O by A7, A8, Th8; :: thesis: verum

end;

end;

end;

hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ; :: thesis: verum

end;

end;

end;

hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ; :: thesis: verum

end;

suppose not HT ((p + q),O) in Support (p + q) ; :: thesis: HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O

then HT ((p + q),O) = EmptyBag n by Def6;
then [(HT ((p + q),O)),(max ((HT (p,O)),(HT (q,O)),O))] in O by BAGORDER:def 5;
hence HT ((p + q),O) <= max ((HT (p,O)),(HT (q,O)),O),O ; :: thesis: verum

end;

end;