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

HM p2,T <> 0_ n,L by POLYNOM7:def 2;
then Support (HM p2,T) <> {} by POLYNOM7:1;
then HT (HM p2,T),T in Support (HM p2,T) by TERMORD:def 6;
then (HM p2,T) . (HT (HM p2,T),T) <> 0. L by POLYNOM1:def 9;
then A11: HC (HM p2,T),T <> 0. L by TERMORD:def 7;
red1 <> 0_ n,L by POLYNOM7:def 2;
then Support red1 <> {} by POLYNOM7:1;
then HT red1,T in Support red1 by TERMORD:def 6;
then red1 . (HT red1,T) <> 0. L by POLYNOM1:def 9;
then HC red1,T <> 0. L by TERMORD:def 7;
then (HC (HM p2,T),T) * (HC red1,T) <> 0. L by A11, VECTSP_2:def 5;
then ( 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, TERMORD:32;
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;
p1 <> 0_ n,L by POLYNOM7:def 2;
then A14: HC p1,T <> 0. L by TERMORD:17;
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 by PRE_POLY:def 12;
( 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 A14, 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 POLYNOM2:sch 4(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: