let n be Ordinal; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis:
let p1, p2 be non-zero Polynomial of n,L; :: thesis:
assume that
A1: HT (p1,T), HT (p2,T) are_disjoint and
A2: ( Red (p1,T) is non-zero & Red (p2,T) is non-zero ) ; :: thesis:
reconsider red1 = Red (p1,T), red2 = Red (p2,T) as non-zero Polynomial of n,L by A2;
set j = card (Support p2);
defpred S₁[ Element of NAT ] means for m being Element of NAT st m <= card (Support p2) & card (Support (Low (p2,T,m))) = $1 holds
PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),(((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,m))))) + ((Red (p1,T)) *' (Low (p2,T,m)));

assume card (Support p2) = 0 ; :: thesis:
then Support p2 = {} ;
then p2 = 0_ (n,L) by POLYNOM7:1;
hence contradiction by POLYNOM7:def 2; :: thesis:

end;

then A3: 1 <= card (Support p2) by NAT_1:14;
then 1 - 1 <= (card (Support p2)) - 1 by XREAL_1:11;
then reconsider j9 = (card (Support p2)) - 1 as Element of NAT by INT_1:16;
A4: (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,1))))) + ((Red (p1,T)) *' (Low (p2,T,1))) = (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Red (p2,T))))) + ((Red (p1,T)) *' (Low (p2,T,1))) by Th36
.= (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (0_ (n,L)))) + ((Red (p1,T)) *' (Low (p2,T,1))) by POLYNOM1:83
.= (((HM (p2,T)) *' (Red (p1,T))) - (0_ (n,L))) + ((Red (p1,T)) *' (Low (p2,T,1))) by POLYRED:5
.= ((HM (p2,T)) *' (Red (p1,T))) + ((Red (p1,T)) *' (Low (p2,T,1))) by POLYRED:4
.= ((HM (p2,T)) *' (Red (p1,T))) + ((Red (p1,T)) *' (Red (p2,T))) by Th36
.= ((HM (p2,T)) + (Red (p2,T))) *' (Red (p1,T)) by POLYNOM1:85
.= p2 *' (Red (p1,T)) by TERMORD:38 ;
p2 <> 0_ (n,L) by POLYNOM7:def 2;
then Support p2 <> {} by POLYNOM7:1;
then HT (p2,T) in Support p2 by TERMORD:def 6;
then for t being set st t in {(HT (p2,T))} holds
t in Support p2 by TARSKI:def 1;
then A5: {(HT (p2,T))} c= Support p2 by TARSKI:def 3;
A6: card (Support red2) = card ((Support p2) \ {(HT (p2,T))}) by TERMORD:36
.= (card (Support p2)) - (card {(HT (p2,T))}) by A5, CARD_2:63
.= (card (Support p2)) - 1 by CARD_2:60 ;
then A7: card (Support (Low (p2,T,1))) = j9 by Th36;
A8: for k being Element of NAT st 0 <= k & k < j9 & S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume that
0 <= k and
A9: k < j9 ; :: thesis:

now

assume A10: S₁[k] ; :: thesis:

now

( HT (((HM (p2,T)) *' red1),T) = (HT ((HM (p2,T)),T)) + (HT (red1,T)) & HC (((HM (p2,T)) *' red1),T) <> 0. L ) by TERMORD:31;
then A12: ((HM (p2,T)) *' red1) . ((HT ((HM (p2,T)),T)) + (HT (red1,T))) <> 0. L by TERMORD:def 7;
A13: Support (Red (p2,T)) c= Support p2 by TERMORD:35;
red2 <> 0_ (n,L) by POLYNOM7:def 2;
then A15: Support red2 <> {} by POLYNOM7:1;
let m be Element of NAT ; :: thesis:
assume that
A16: m <= card (Support p2) and
A17: card (Support (Low (p2,T,m))) = k + 1 ; :: thesis:
set m9 = m + 1;

now

assume m = card (Support p2) ; :: thesis:
then Low (p2,T,m) = 0_ (n,L) by Th35;
hence contradiction by A17, CARD_1:47, POLYNOM7:1; :: thesis:

end;

then A18: m < card (Support p2) by A16, XXREAL_0:1;
then card ((Support (Low (p2,T,m))) \ (Support (Low (p2,T,(m + 1))))) = (card (Support (Low (p2,T,m)))) - (card (Support (Low (p2,T,(m + 1))))) by Th41, CARD_2:63;
then A19: (k + 1) - (card (Support (Low (p2,T,(m + 1))))) = card {(HT ((Low (p2,T,m)),T))} by A17, A18, Th42
.= 1 by CARD_1:50 ;
set f = (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))));
A20: (HT ((HM (p2,T)),T)) + (HT (red1,T)) is Element of Bags n by PRE_POLY:def 12;
A21: m + 1 <= card (Support p2) by A18, NAT_1:13;

now

A22: Support (red1 *' (Low (p2,T,(m + 1)))) c= { (s + t) where s, t is Element of Bags n : ( s in Support red1 & t in Support (Low (p2,T,(m + 1))) ) } by TERMORD:30;
assume (HT ((HM (p2,T)),T)) + (HT (red1,T)) in Support (red1 *' (Low (p2,T,(m + 1)))) ; :: thesis:
then (HT ((HM (p2,T)),T)) + (HT (red1,T)) in { (s + t) where s, t is Element of Bags n : ( s in Support red1 & t in Support (Low (p2,T,(m + 1))) ) } by A22;
then consider s, t being Element of Bags n such that
A23: (HT ((HM (p2,T)),T)) + (HT (red1,T)) = s + t and
A24: s in Support red1 and
A25: t in Support (Low (p2,T,(m + 1))) ;
A26: t < HT (p2,T),T

proof

now

per cases ;

case m + 1 = card (Support p2) ; :: thesis:

then Low (p2,T,(m + 1)) = 0_ (n,L) by Th35;
hence contradiction by A25, POLYNOM7:1; :: thesis:

end;

case A27: m + 1 <> card (Support p2) ; :: thesis:

A28: t <= HT ((Low (p2,T,(m + 1))),T),T by A25, TERMORD:def 6;
m + 1 < card (Support p2) by A21, A27, XXREAL_0:1;
hence t < HT (p2,T),T by A28, Th3, Th39; :: thesis:

end;

hence t < HT (p2,T),T ; :: thesis:

end;

s <= HT (red1,T),T by A24, TERMORD:def 6;
then s + t < (HT (p2,T)) + (HT (red1,T)),T by A26, Th5;
then s + t < (HT ((HM (p2,T)),T)) + (HT (red1,T)),T by TERMORD:26;
hence contradiction by A23, TERMORD:def 3; :: thesis:

end;

then A29: (red1 *' (Low (p2,T,(m + 1)))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T))) = 0. L by A20, POLYNOM1:def 9;
A30: 1 <= m + 1 by NAT_1:14;

now

red1 <> 0_ (n,L) by POLYNOM7:def 2;
then Support red1 <> {} by POLYNOM7:1;
then A31: ( HT ((HM (p2,T)),T) = HT (p2,T) & HT (red1,T) in Support red1 ) by TERMORD:26, TERMORD:def 6;
A32: Support ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))) c= { (s + t) where s, t is Element of Bags n : ( s in Support (HM (p1,T)) & t in Support (red2 - (Low (p2,T,(m + 1)))) ) } by TERMORD:30;
assume (HT ((HM (p2,T)),T)) + (HT (red1,T)) in Support ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))) ; :: thesis:
then A33: (HT ((HM (p2,T)),T)) + (HT (red1,T)) in { (s + t) where s, t is Element of Bags n : ( s in Support (HM (p1,T)) & t in Support (red2 - (Low (p2,T,(m + 1)))) ) } by A32;
( red2 - (Low (p2,T,(m + 1))) = red2 + (- (Low (p2,T,(m + 1)))) & Support (- (Low (p2,T,(m + 1)))) = Support (Low (p2,T,(m + 1))) ) by GROEB_1:5, POLYNOM1:def 23;
then A34: Support (red2 - (Low (p2,T,(m + 1)))) c= (Support red2) \/ (Support (Low (p2,T,(m + 1)))) by POLYNOM1:79;
consider s, t being Element of Bags n such that
A35: (HT ((HM (p2,T)),T)) + (HT (red1,T)) = s + t and
A36: s in Support (HM (p1,T)) and
A37: t in Support (red2 - (Low (p2,T,(m + 1)))) by A33;
A38: Support (Low (p2,T,(m + 1))) c= Support red2 by A21, A30, Th27;
A39: t in Support red2

proof

now

per cases by A37, A34, XBOOLE_0:def 3;

case t in Support red2 ; :: thesis:

hence t in Support red2 ; :: thesis:

end;

case t in Support (Low (p2,T,(m + 1))) ; :: thesis:

hence t in Support red2 by A38; :: thesis:

end;

hence t in Support red2 ; :: thesis:

end;

HM (p1,T) <> 0_ (n,L) by POLYNOM7:def 2;
then Support (HM (p1,T)) <> {} by POLYNOM7:1;
then Support (HM (p1,T)) = {(HT (p1,T))} by TERMORD:21;
then s = HT (p1,T) by A36, TARSKI:def 1;
hence contradiction by A1, A35, A31, A39, Th52; :: thesis:

end;

then ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T))) = 0. L by A20, POLYNOM1:def 9;
then A40: - (((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T)))) = 0. L by RLVECT_1:25;
A41: Support (Low (p2,T,(m + 1))) = Lower_Support (p2,T,(m + 1)) by A21, Lm3;

now

assume A42: HT (red2,T) in Support (Low (p2,T,(m + 1))) ; :: thesis:

A43: now

let t be set ; :: thesis:
assume A44: t in Support red2 ; :: thesis:
then reconsider t9 = t as bag of n ;
( Support red2 c= Support p2 & t9 <= HT (red2,T),T ) by A44, TERMORD:35, TERMORD:def 6;
hence t in Support (Low (p2,T,(m + 1))) by A21, A41, A42, A44, Th24; :: thesis:

end;

Support (Low (p2,T,(m + 1))) c= Support red2 by A21, A30, Th27;
then for t being set st t in Support (Low (p2,T,(m + 1))) holds
t in Support red2 ;
hence contradiction by A6, A9, A19, A43, TARSKI:2; :: thesis:

end;

then Low (p2,T,(m + 1)) <> red2 by A15, TERMORD:def 6;
then (Red (p2,T)) - (Low (p2,T,(m + 1))) <> 0_ (n,L) by Th12;
then reconsider z1 = (Red (p2,T)) - (Low (p2,T,(m + 1))) as non-zero Polynomial of n,L by POLYNOM7:def 2;
reconsider z = (HM (p1,T)) *' z1 as non-zero Polynomial of n,L ;
z1 = (Red (p2,T)) + (- (Low (p2,T,(m + 1)))) by POLYNOM1:def 23;
then Support z1 c= (Support (Red (p2,T))) \/ (Support (- (Low (p2,T,(m + 1))))) by POLYNOM1:79;
then A45: Support z1 c= (Support (Red (p2,T))) \/ (Support (Low (p2,T,(m + 1)))) by GROEB_1:5;
z <> 0_ (n,L) by POLYNOM7:def 2;
then Support z <> {} by POLYNOM7:1;
then reconsider w = (card (Support z)) - 1 as Element of NAT by INT_1:18, NAT_1:14;
reconsider lowzw = Low (z,T,w) as non-zero Monomial of n,L by Th37;
set b = term lowzw;
set s = (term lowzw) / (HT (p1,T));
A46: Support ((HM (p1,T)) *' z1) c= { (t9 + t) where t9, t is Element of Bags n : ( t9 in Support (HM (p1,T)) & t in Support z1 ) } by TERMORD:30;
card (Support z) = w + 1 ;
then A47: w < card (Support z) by NAT_1:16;
then A48: Support lowzw c= Support z by Th26;
lowzw <> 0_ (n,L) by POLYNOM7:def 2;
then Support lowzw <> {} by POLYNOM7:1;
then Support lowzw = {(term lowzw)} by POLYNOM7:7;
then A49: term lowzw in Support lowzw by TARSKI:def 1;
then term lowzw in Support ((HM (p1,T)) *' z1) by A48;
then term lowzw in { (t9 + t) where t9, t is Element of Bags n : ( t9 in Support (HM (p1,T)) & t in Support z1 ) } by A46;
then consider t9, t being Element of Bags n such that
A50: term lowzw = t9 + t and
A51: t9 in Support (HM (p1,T)) and
A52: t in Support z1 ;
HM (p1,T) <> 0_ (n,L) by POLYNOM7:def 2;
then Support (HM (p1,T)) <> {} by POLYNOM7:1;
then Support (HM (p1,T)) = {(term (HM (p1,T)))} by POLYNOM7:7
.= {(HT (p1,T))} by TERMORD:22 ;
then A53: t9 = HT (p1,T) by A51, TARSKI:def 1;
then A54: HT (p1,T) divides term lowzw by A50, PRE_POLY:50;
then A55: ((term lowzw) / (HT (p1,T))) + (HT (p1,T)) = term lowzw by GROEB_2:def 1;
A56: (term lowzw) / (HT (p1,T)) = (((term lowzw) / (HT (p1,T))) + (HT (p1,T))) -' (HT (p1,T)) by PRE_POLY:48
.= t by A50, A53, A55, PRE_POLY:48 ;
(Support (Red (p2,T))) \/ (Support (Low (p2,T,(m + 1)))) c= (Support (Red (p2,T))) \/ (Support (Red (p2,T))) by A21, A30, Th27, XBOOLE_1:9;
then A57: Support z1 c= Support red2 by A45, XBOOLE_1:1;
then A58: (term lowzw) / (HT (p1,T)) in Support (Red (p2,T)) by A52, A56;
then (term lowzw) / (HT (p1,T)) in (Support p2) \ {(HT (p2,T))} by TERMORD:36;
then not (term lowzw) / (HT (p1,T)) in {(HT (p2,T))} by XBOOLE_0:def 5;
then A59: (term lowzw) / (HT (p1,T)) <> HT (p2,T) by TARSKI:def 1;
then A60: (Red (p2,T)) . ((term lowzw) / (HT (p1,T))) = p2 . ((term lowzw) / (HT (p1,T))) by A58, A13, TERMORD:40;

A61: now

assume (term lowzw) / (HT (p1,T)) in Support (Low (p2,T,(m + 1))) ; :: thesis:
then A62: p2 . ((term lowzw) / (HT (p1,T))) = (Low (p2,T,(m + 1))) . ((term lowzw) / (HT (p1,T))) by Th16;
((Red (p2,T)) - (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T))) = ((Red (p2,T)) + (- (Low (p2,T,(m + 1))))) . ((term lowzw) / (HT (p1,T))) by POLYNOM1:def 23
.= ((Red (p2,T)) . ((term lowzw) / (HT (p1,T)))) + ((- (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T)))) by POLYNOM1:def 21
.= ((Red (p2,T)) . ((term lowzw) / (HT (p1,T)))) + (- ((Low (p2,T,(m + 1))) . ((term lowzw) / (HT (p1,T))))) by POLYNOM1:def 22
.= 0. L by A60, A62, RLVECT_1:16 ;
hence contradiction by A52, A56, POLYNOM1:def 9; :: thesis:

end;

A63: term lowzw is Element of Bags n by PRE_POLY:def 12;

A64: now

assume ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) . (term lowzw) <> 0. L ; :: thesis:
then A65: term lowzw in Support ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) by A63, POLYNOM1:def 9;
Support ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) c= { (u + v) where u, v is Element of Bags n : ( u in Support (Red (p1,T)) & v in Support (Low (p2,T,(m + 1))) ) } by TERMORD:30;
then term lowzw in { (u + v) where u, v is Element of Bags n : ( u in Support (Red (p1,T)) & v in Support (Low (p2,T,(m + 1))) ) } by A65;
then consider t9, t being Element of Bags n such that
A66: term lowzw = t9 + t and
A67: t9 in Support (Red (p1,T)) and
A68: t in Support (Low (p2,T,(m + 1))) ;
A69: ((term lowzw) / (HT (p1,T))) + (HT (p1,T)) = t9 + t by A54, A66, GROEB_2:def 1;

now

assume (term lowzw) / (HT (p1,T)) < t,T ; :: thesis:
then A70: (term lowzw) / (HT (p1,T)) <= t,T by TERMORD:def 3;
t in Lower_Support (p2,T,(m + 1)) by A21, A68, Lm3;
then (term lowzw) / (HT (p1,T)) in Lower_Support (p2,T,(m + 1)) by A21, A58, A13, A70, Th24;
hence contradiction by A21, A61, Lm3; :: thesis:

end;

then A71: t <= (term lowzw) / (HT (p1,T)),T by TERMORD:5;
Support (Red (p1,T)) = (Support p1) \ {(HT (p1,T))} by TERMORD:36;
then not t9 in {(HT (p1,T))} by A67, XBOOLE_0:def 5;
then A72: t9 <> HT (p1,T) by TARSKI:def 1;
Support (Red (p1,T)) c= Support p1 by TERMORD:35;
then t9 <= HT (p1,T),T by A67, TERMORD:def 6;
then t9 < HT (p1,T),T by A72, TERMORD:def 3;
then t + t9 < ((term lowzw) / (HT (p1,T))) + (HT (p1,T)),T by A71, Th6;
hence contradiction by A69, TERMORD:def 3; :: thesis:

end;

A73: now

HM (p2,T) <> 0_ (n,L) by POLYNOM7:def 2;
then A74: Support (HM (p2,T)) <> {} by POLYNOM7:1;
then HT ((HM (p2,T)),T) in Support (HM (p2,T)) by TERMORD:def 6;
then A75: HT (p2,T) in Support (HM (p2,T)) by TERMORD:26;
A76: Support ((HM (p2,T)) *' (Red (p1,T))) c= { (u + v) where u, v is Element of Bags n : ( u in Support (HM (p2,T)) & v in Support (Red (p1,T)) ) } by TERMORD:30;
assume term lowzw in Support ((HM (p2,T)) *' (Red (p1,T))) ; :: thesis:
then term lowzw in { (u + v) where u, v is Element of Bags n : ( u in Support (HM (p2,T)) & v in Support (Red (p1,T)) ) } by A76;
then consider t9, t being Element of Bags n such that
A77: term lowzw = t9 + t and
A78: t9 in Support (HM (p2,T)) and
A79: t in Support (Red (p1,T)) ;
ex x being bag of n st Support (HM (p2,T)) = {x} by A74, POLYNOM7:6;
then Support (HM (p2,T)) = {(HT (p2,T))} by A75, TARSKI:def 1;
then t9 = HT (p2,T) by A78, TARSKI:def 1;
hence contradiction by A1, A57, A52, A55, A56, A77, A79, Th52; :: thesis:

end;

set g = ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) - (((((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . (term lowzw)) / (HC (p1,T))) * (((term lowzw) / (HT (p1,T))) *' p1));
A80: (HT ((HM (p2,T)),T)) + (HT (red1,T)) is Element of Bags n by PRE_POLY:def 12;
A81: ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . (term lowzw) = ((((HM (p2,T)) *' red1) + (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))))) + (red1 *' (Low (p2,T,(m + 1))))) . (term lowzw) by POLYNOM1:def 23
.= ((((HM (p2,T)) *' red1) + (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))))) . (term lowzw)) + (0. L) by A64, POLYNOM1:def 21
.= (((HM (p2,T)) *' red1) + (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))))) . (term lowzw) by RLVECT_1:def 7
.= (((HM (p2,T)) *' red1) . (term lowzw)) + ((- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1)))))) . (term lowzw)) by POLYNOM1:def 21
.= (0. L) + ((- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1)))))) . (term lowzw)) by A63, A73, POLYNOM1:def 9
.= (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1)))))) . (term lowzw) by RLVECT_1:def 7
.= - (((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))) . (term lowzw)) by POLYNOM1:def 22 ;
w = (card (Support z1)) - 1 by Th10;
then reconsider lowz1w = Low (z1,T,w) as non-zero Monomial of n,L by Th37;
w + 1 = ((card (Support z1)) - 1) + 1 by Th10;
then A82: w <= card (Support z1) by NAT_1:13;
lowz1w <> 0_ (n,L) by POLYNOM7:def 2;
then Support lowz1w <> {} by POLYNOM7:1;
then A83: Support lowz1w = {(term lowz1w)} by POLYNOM7:7;
card (Support z) = card (Support z1) by Th10;
then ((term lowzw) / (HT (p1,T))) + (HT (p1,T)) = term ((HM (p1,T)) *' lowz1w) by A47, A55, Th44
.= (term (HM (p1,T))) + (term lowz1w) by Th7
.= (HT (p1,T)) + (term lowz1w) by TERMORD:22 ;
then A84: (term lowzw) / (HT (p1,T)) = ((HT (p1,T)) + (term lowz1w)) -' (HT (p1,T)) by PRE_POLY:48
.= term lowz1w by PRE_POLY:48 ;
then (term lowzw) / (HT (p1,T)) in Support lowz1w by A83, TARSKI:def 1;
then A85: (term lowzw) / (HT (p1,T)) in Lower_Support (z1,T,w) by A82, Lm3;
Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T)))) = HM ((Low (p2,T,m)),T)

proof

A86: now

let t be bag of n; :: thesis:
assume A87: t in Support z1 ; :: thesis:

now

assume A88: t < (term lowzw) / (HT (p1,T)),T ; :: thesis:
then t <= (term lowzw) / (HT (p1,T)),T by TERMORD:def 3;
then t in Lower_Support (z1,T,w) by A82, A85, A87, Th24;
then t in Support lowz1w by A82, Lm3;
then t = term lowz1w by A83, TARSKI:def 1;
hence contradiction by A84, A88, TERMORD:def 3; :: thesis:

end;

hence (term lowzw) / (HT (p1,T)) <= t,T by TERMORD:5; :: thesis:

end;

set r = HT ((Low (p2,T,m)),T);
(Support (Low (p2,T,m))) \ (Support (Low (p2,T,(m + 1)))) = {(HT ((Low (p2,T,m)),T))} by A18, Th42;
then A89: HT ((Low (p2,T,m)),T) in (Support (Low (p2,T,m))) \ (Support (Low (p2,T,(m + 1)))) by TARSKI:def 1;
then A90: not HT ((Low (p2,T,m)),T) in Support (Low (p2,T,(m + 1))) by XBOOLE_0:def 5;
A91: ((Red (p2,T)) - (Low (p2,T,(m + 1)))) . (HT ((Low (p2,T,m)),T)) = ((Red (p2,T)) + (- (Low (p2,T,(m + 1))))) . (HT ((Low (p2,T,m)),T)) by POLYNOM1:def 23
.= ((Red (p2,T)) . (HT ((Low (p2,T,m)),T))) + ((- (Low (p2,T,(m + 1)))) . (HT ((Low (p2,T,m)),T))) by POLYNOM1:def 21
.= ((Red (p2,T)) . (HT ((Low (p2,T,m)),T))) + (- ((Low (p2,T,(m + 1))) . (HT ((Low (p2,T,m)),T)))) by POLYNOM1:def 22
.= ((Red (p2,T)) . (HT ((Low (p2,T,m)),T))) + (- (0. L)) by A90, POLYNOM1:def 9
.= ((Red (p2,T)) . (HT ((Low (p2,T,m)),T))) + (0. L) by RLVECT_1:25
.= (Red (p2,T)) . (HT ((Low (p2,T,m)),T)) by RLVECT_1:def 7 ;
A92: HT ((Low (p2,T,m)),T) in Support (Low (p2,T,m)) by A89, XBOOLE_0:def 5;
then A93: HT ((Low (p2,T,m)),T) in Lower_Support (p2,T,m) by A16, Lm3;
A94: Support (Low (p2,T,m)) c= Support p2 by A16, Th26;

now

assume A95: HT ((Low (p2,T,m)),T) = HT (p2,T) ; :: thesis:

A96: now

let u be set ; :: thesis:
assume A97: u in Support p2 ; :: thesis:
then reconsider u9 = u as Element of Bags n ;
u9 <= HT ((Low (p2,T,m)),T),T by A95, A97, TERMORD:def 6;
then u9 in Lower_Support (p2,T,m) by A16, A93, A97, Th24;
hence u in Support (Low (p2,T,m)) by A16, Lm3; :: thesis:

end;

for u being set st u in Support (Low (p2,T,m)) holds
u in Support p2 by A94;
then k + 1 = card (Support p2) by A17, A96, TARSKI:2;
hence contradiction by A9; :: thesis:

end;

then A98: not HT ((Low (p2,T,m)),T) in {(HT (p2,T))} by TARSKI:def 1;
Support (Red (p2,T)) = (Support p2) \ {(HT (p2,T))} by TERMORD:36;
then HT ((Low (p2,T,m)),T) in Support red2 by A92, A94, A98, XBOOLE_0:def 5;
then z1 . (HT ((Low (p2,T,m)),T)) <> 0. L by A91, POLYNOM1:def 9;
then A99: HT ((Low (p2,T,m)),T) in Support z1 by POLYNOM1:def 9;
Support red2 c= Support p2 by TERMORD:35;
then (term lowzw) / (HT (p1,T)) in Lower_Support (p2,T,m) by A16, A58, A86, A93, A99, Th24;
then A100: (term lowzw) / (HT (p1,T)) in Support (Low (p2,T,m)) by A16, Lm3;
then (term lowzw) / (HT (p1,T)) in (Support (Low (p2,T,m))) \ (Support (Low (p2,T,(m + 1)))) by A61, XBOOLE_0:def 5;
then (term lowzw) / (HT (p1,T)) in {(HT ((Low (p2,T,m)),T))} by A18, Th42;
then A101: (term lowzw) / (HT (p1,T)) = HT ((Low (p2,T,m)),T) by TARSKI:def 1;
then A102: (HM ((Low (p2,T,m)),T)) . (HT ((Low (p2,T,m)),T)) = (Low (p2,T,m)) . ((term lowzw) / (HT (p1,T))) by TERMORD:18
.= p2 . ((term lowzw) / (HT (p1,T))) by A16, A100, Th31 ;
HC ((Low (p2,T,m)),T) = (Low (p2,T,m)) . (HT ((Low (p2,T,m)),T)) by TERMORD:def 7
.= p2 . ((term lowzw) / (HT (p1,T))) by A102, TERMORD:18 ;
hence Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T)))) = HM ((Low (p2,T,m)),T) by A101, TERMORD:def 8; :: thesis:

end;

then A103: Low (p2,T,m) = (Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) + (Red ((Low (p2,T,m)),T)) by TERMORD:38
.= (Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) + (Low (p2,T,(m + 1))) by A18, Th43 ;
A104: ((HM (p1,T)) *' z1) . (term lowzw) <> 0. L by A49, A48, POLYNOM1:def 9;

now

assume ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . (term lowzw) = 0. L ; :: thesis:
then ((HM (p1,T)) *' z1) . (term lowzw) = - (0. L) by A81, RLVECT_1:30;
hence contradiction by A104, RLVECT_1:25; :: thesis:

end;

then A105: ( p1 <> 0_ (n,L) & term lowzw in Support ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) ) by A63, POLYNOM1:def 9, POLYNOM7:def 2;
((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T))) = ((((HM (p2,T)) *' red1) + (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))))) + (red1 *' (Low (p2,T,(m + 1))))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T))) by POLYNOM1:def 23
.= ((((HM (p2,T)) *' red1) + (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T)))) + (0. L) by A29, POLYNOM1:def 21
.= (((HM (p2,T)) *' red1) + (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T))) by RLVECT_1:def 7
.= (((HM (p2,T)) *' red1) . ((HT ((HM (p2,T)),T)) + (HT (red1,T)))) + ((- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1)))))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T)))) by POLYNOM1:def 21
.= (((HM (p2,T)) *' red1) . ((HT ((HM (p2,T)),T)) + (HT (red1,T)))) + (0. L) by A40, POLYNOM1:def 22
.= ((HM (p2,T)) *' red1) . ((HT ((HM (p2,T)),T)) + (HT (red1,T))) by RLVECT_1:def 7 ;
then (HT ((HM (p2,T)),T)) + (HT (red1,T)) in Support ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) by A12, A80, POLYNOM1:def 9;
then (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) <> 0_ (n,L) by POLYNOM7:1;
then (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) reduces_to ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) - (((((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . (term lowzw)) / (HC (p1,T))) * (((term lowzw) / (HT (p1,T))) *' p1)),p1, term lowzw,T by A55, A105, POLYRED:def 5;
then A106: (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) reduces_to ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) - (((((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . (term lowzw)) / (HC (p1,T))) * (((term lowzw) / (HT (p1,T))) *' p1)),p1,T by POLYRED:def 6;
p1 in {p1} by TARSKI:def 1;
then (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) reduces_to ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) - (((((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . (term lowzw)) / (HC (p1,T))) * (((term lowzw) / (HT (p1,T))) *' p1)),{p1},T by A106, POLYRED:def 7;
then [((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))),(((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) - (((((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . (term lowzw)) / (HC (p1,T))) * (((term lowzw) / (HT (p1,T))) *' p1)))] in PolyRedRel ({p1},T) by POLYRED:def 13;
then A107: PolyRedRel ({p1},T) reduces (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1)))),((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) - (((((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . (term lowzw)) / (HC (p1,T))) * (((term lowzw) / (HT (p1,T))) *' p1)) by REWRITE1:16;
m + 1 <= card (Support p2) by A18, NAT_1:13;
then A108: PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),(((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) by A10, A19;
A109: HT (p1,T) = HT ((HM (p1,T)),T) by TERMORD:26
.= term (HM (p1,T)) by TERMORD:23 ;
(term lowzw) / (HT (p1,T)) is Element of Bags n by PRE_POLY:def 12;
then A110: (Low (p2,T,(m + 1))) . ((term lowzw) / (HT (p1,T))) = 0. L by A61, POLYNOM1:def 9;
((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))) . (term lowzw) = ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))) . (((term lowzw) / (HT (p1,T))) + (HT (p1,T))) by A54, GROEB_2:def 1
.= ((HM (p1,T)) . (HT (p1,T))) * ((red2 - (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T)))) by A109, POLYRED:7
.= (p1 . (HT (p1,T))) * ((red2 - (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T)))) by TERMORD:18
.= (HC (p1,T)) * ((red2 - (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T)))) by TERMORD:def 7
.= (HC (p1,T)) * ((red2 + (- (Low (p2,T,(m + 1))))) . ((term lowzw) / (HT (p1,T)))) by POLYNOM1:def 23
.= (HC (p1,T)) * ((red2 . ((term lowzw) / (HT (p1,T)))) + ((- (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T))))) by POLYNOM1:def 21
.= (HC (p1,T)) * ((p2 . ((term lowzw) / (HT (p1,T)))) + ((- (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T))))) by A58, A13, A59, TERMORD:40
.= (HC (p1,T)) * ((p2 . ((term lowzw) / (HT (p1,T)))) + (- ((Low (p2,T,(m + 1))) . ((term lowzw) / (HT (p1,T)))))) by POLYNOM1:def 22
.= (HC (p1,T)) * ((p2 . ((term lowzw) / (HT (p1,T)))) + (0. L)) by A110, RLVECT_1:25
.= (HC (p1,T)) * (p2 . ((term lowzw) / (HT (p1,T)))) by RLVECT_1:def 7 ;
then ((((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . (term lowzw)) / (HC (p1,T))) * (((term lowzw) / (HT (p1,T))) *' p1) = (((HC (p1,T)) * (- (p2 . ((term lowzw) / (HT (p1,T)))))) / (HC (p1,T))) * (((term lowzw) / (HT (p1,T))) *' p1) by A81, VECTSP_1:41
.= (((HC (p1,T)) * (- (p2 . ((term lowzw) / (HT (p1,T)))))) * ((HC (p1,T)) ")) * (((term lowzw) / (HT (p1,T))) *' p1) by VECTSP_1:def 23
.= ((- (p2 . ((term lowzw) / (HT (p1,T))))) * ((HC (p1,T)) * ((HC (p1,T)) "))) * (((term lowzw) / (HT (p1,T))) *' p1) by GROUP_1:def 4
.= ((- (p2 . ((term lowzw) / (HT (p1,T))))) * (1. L)) * (((term lowzw) / (HT (p1,T))) *' p1) by VECTSP_1:def 22
.= (- (p2 . ((term lowzw) / (HT (p1,T))))) * (((term lowzw) / (HT (p1,T))) *' p1) by VECTSP_1:def 16 ;
then ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) - (((((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) . (term lowzw)) / (HC (p1,T))) * (((term lowzw) / (HT (p1,T))) *' p1)) = ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + (- ((- (p2 . ((term lowzw) / (HT (p1,T))))) * (((term lowzw) / (HT (p1,T))) *' p1))) by POLYNOM1:def 23
.= ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + ((- (- (p2 . ((term lowzw) / (HT (p1,T)))))) * (((term lowzw) / (HT (p1,T))) *' p1)) by POLYRED:9
.= ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + ((p2 . ((term lowzw) / (HT (p1,T)))) * (((term lowzw) / (HT (p1,T))) *' p1)) by RLVECT_1:30
.= ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' p1) by POLYRED:22
.= ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' ((HM (p1,T)) + (Red (p1,T)))) by TERMORD:38
.= ((((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + (((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (HM (p1,T))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (Red (p1,T)))) by POLYNOM1:85
.= ((((HM (p2,T)) *' (Red (p1,T))) + (- ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1))))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + (((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (HM (p1,T))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (Red (p1,T)))) by POLYNOM1:def 23
.= (((((HM (p2,T)) *' (Red (p1,T))) + (- ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1))))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (HM (p1,T)))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (Red (p1,T))) by POLYNOM1:80
.= (((((HM (p2,T)) *' (Red (p1,T))) + (- ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,(m + 1))))))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (HM (p1,T)))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (Red (p1,T))) by POLYNOM1:80
.= (((((HM (p2,T)) *' (Red (p1,T))) + ((HM (p1,T)) *' (- ((Red (p2,T)) - (Low (p2,T,(m + 1))))))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (HM (p1,T)))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (Red (p1,T))) by POLYRED:6
.= ((((HM (p2,T)) *' (Red (p1,T))) + (((HM (p1,T)) *' (- ((Red (p2,T)) - (Low (p2,T,(m + 1)))))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (HM (p1,T))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (Red (p1,T))) by POLYNOM1:80
.= ((((HM (p2,T)) *' (Red (p1,T))) + ((HM (p1,T)) *' ((- ((Red (p2,T)) - (Low (p2,T,(m + 1))))) + (Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T)))))))) + ((Red (p1,T)) *' (Low (p2,T,(m + 1))))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (Red (p1,T))) by POLYNOM1:85
.= (((HM (p2,T)) *' (Red (p1,T))) + ((HM (p1,T)) *' ((- ((Red (p2,T)) - (Low (p2,T,(m + 1))))) + (Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T)))))))) + (((Red (p1,T)) *' (Low (p2,T,(m + 1)))) + ((Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T))))) *' (Red (p1,T)))) by POLYNOM1:80
.= (((HM (p2,T)) *' (Red (p1,T))) + ((HM (p1,T)) *' ((- ((Red (p2,T)) - (Low (p2,T,(m + 1))))) + (Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T)))))))) + ((Red (p1,T)) *' (Low (p2,T,m))) by A103, POLYNOM1:85
.= (((HM (p2,T)) *' (Red (p1,T))) + ((HM (p1,T)) *' ((- ((Red (p2,T)) + (- (Low (p2,T,(m + 1)))))) + (Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T)))))))) + ((Red (p1,T)) *' (Low (p2,T,m))) by POLYNOM1:def 23
.= (((HM (p2,T)) *' (Red (p1,T))) + ((HM (p1,T)) *' (((- (Red (p2,T))) + (- (- (Low (p2,T,(m + 1)))))) + (Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T)))))))) + ((Red (p1,T)) *' (Low (p2,T,m))) by POLYRED:1
.= (((HM (p2,T)) *' (Red (p1,T))) + ((HM (p1,T)) *' ((- (Red (p2,T))) + (- (- (Low (p2,T,m))))))) + ((Red (p1,T)) *' (Low (p2,T,m))) by A103, POLYNOM1:80
.= (((HM (p2,T)) *' (Red (p1,T))) + ((HM (p1,T)) *' (- ((Red (p2,T)) + (- (Low (p2,T,m))))))) + ((Red (p1,T)) *' (Low (p2,T,m))) by POLYRED:1
.= (((HM (p2,T)) *' (Red (p1,T))) + ((HM (p1,T)) *' (- ((Red (p2,T)) - (Low (p2,T,m)))))) + ((Red (p1,T)) *' (Low (p2,T,m))) by POLYNOM1:def 23
.= (((HM (p2,T)) *' (Red (p1,T))) + (- ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,m)))))) + ((Red (p1,T)) *' (Low (p2,T,m))) by POLYRED:6
.= (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,m))))) + ((Red (p1,T)) *' (Low (p2,T,m))) by POLYNOM1:def 23 ;
hence PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),(((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,m))))) + ((Red (p1,T)) *' (Low (p2,T,m))) by A107, A108, REWRITE1:17; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

hence ( not S₁[k] or S₁[k + 1] ) ; :: thesis:

end;

A111: S₁[ 0 ]

proof

let m be Element of NAT ; :: thesis:
assume that
m <= card (Support p2) and
A112: card (Support (Low (p2,T,m))) = 0 ; :: thesis:
Support (Low (p2,T,m)) = {} by A112;
then Low (p2,T,m) = 0_ (n,L) by POLYNOM7:1;
then (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,m))))) + ((Red (p1,T)) *' (Low (p2,T,m))) = (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T)))) + ((Red (p1,T)) *' (0_ (n,L))) by POLYRED:4
.= (((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T)))) + (0_ (n,L)) by POLYRED:5
.= ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))) by POLYRED:2 ;
hence PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),(((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' ((Red (p2,T)) - (Low (p2,T,m))))) + ((Red (p1,T)) *' (Low (p2,T,m))) by REWRITE1:13; :: thesis:

end;

for i being Element of NAT st 0 <= i & i <= j9 holds
S₁[i] from INT_1:sch 7(A111, A8);
hence PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),p2 *' (Red (p1,T)) by A3, A7, A4; :: thesis: