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 A1: ( HT p1,T, HT p2,T are_disjoint & Red p1,T is non-zero & Red p2,T is non-zero ) ; :: thesis:
then reconsider red1 = Red p1,T, red2 = Red p2,T as non-zero Polynomial of n,L ;
set j = card (Support p2);
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 A2: {(HT p2,T)} c= Support p2 by TARSKI:def 3;
A3: card (Support red2) = card ((Support p2) \ {(HT p2,T)}) by TERMORD:36
.= (card (Support p2)) - (card {(HT p2,T)}) by A2, CARD_2:63
.= (card (Support p2)) - 1 by CARD_2:60 ;

now

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

end;

then A4: 1 <= card (Support p2) by NAT_1:14;
then 1 - 1 <= (card (Support p2)) - 1 by XREAL_1:11;
then reconsider j' = (card (Support p2)) - 1 as Element of NAT by INT_1:16;
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));
A5: S₁[ 0 ]

proof

let m be Element of NAT ; :: thesis:
assume ( m <= card (Support p2) & card (Support (Low p2,T,m)) = 0 ) ; :: thesis:
then Support (Low p2,T,m), 0 are_equipotent by CARD_1:def 5;
then Support (Low p2,T,m) = {} by CARD_1:46;
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;

A6: for k being Element of NAT st 0 <= k & k < j' & S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A7: ( 0 <= k & k < j' ) ; :: thesis:

now

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

now

let m be Element of NAT ; :: thesis:
assume A9: ( m <= card (Support p2) & card (Support (Low p2,T,m)) = k + 1 ) ; :: thesis:
set m' = m + 1;

now

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

end;

then A10: m < card (Support p2) by A9, XXREAL_0:1;
then A11: m + 1 <= card (Support p2) by NAT_1:13;
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 A10, Th41, CARD_2:63;
then A12: (k + 1) - (card (Support (Low p2,T,(m + 1)))) = card {(HT (Low p2,T,m),T)} by A9, A10, Th42
.= 1 by CARD_1:50 ;
then A13: ( m + 1 <= card (Support p2) & card (Support (Low p2,T,(m + 1))) = k ) by A10, NAT_1:13;
A14: 1 <= m + 1 by NAT_1:14;
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)));
( red1 <> 0_ n,L & HM p2,T <> 0_ n,L ) by POLYNOM7:def 2;
then ( Support red1 <> {} & Support (HM p2,T) <> {} ) by POLYNOM7:1;
then ( HT red1,T in Support red1 & HT (HM p2,T),T in Support (HM p2,T) ) by TERMORD:def 6;
then ( red1 . (HT red1,T) <> 0. L & (HM p2,T) . (HT (HM p2,T),T) <> 0. L ) by POLYNOM1:def 9;
then ( HC red1,T <> 0. L & HC (HM p2,T),T <> 0. L ) by TERMORD:def 7;
then A15: (HC (HM p2,T),T) * (HC red1,T) <> 0. L by VECTSP_2:def 5;
A16: HT ((HM p2,T) *' red1),T = (HT (HM p2,T),T) + (HT red1,T) by TERMORD:31;
HC ((HM p2,T) *' red1),T <> 0. L by A15, TERMORD:32;
then A17: ((HM p2,T) *' red1) . ((HT (HM p2,T),T) + (HT red1,T)) <> 0. L by A16, TERMORD:def 7;
A18: (HT (HM p2,T),T) + (HT red1,T) is Element of Bags n by POLYNOM1:def 14;

now

assume A19: (HT (HM p2,T),T) + (HT red1,T) in Support (red1 *' (Low p2,T,(m + 1))) ; :: thesis:
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;
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 A19;
then consider s, t being Element of Bags n such that
A20: ( (HT (HM p2,T),T) + (HT red1,T) = s + t & s in Support red1 & t in Support (Low p2,T,(m + 1)) ) ;
A21: 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 A20, POLYNOM7:1; :: thesis:

end;

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

then A22: m + 1 < card (Support p2) by A11, XXREAL_0:1;
t <= HT (Low p2,T,(m + 1)),T,T by A20, TERMORD:def 6;
hence t < HT p2,T,T by A22, Th3, Th39; :: thesis:

end;

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

end;

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

end;

then A23: (red1 *' (Low p2,T,(m + 1))) . ((HT (HM p2,T),T) + (HT red1,T)) = 0. L by A18, POLYNOM1:def 9;

now

assume A24: (HT (HM p2,T),T) + (HT red1,T) in Support ((HM p1,T) *' (red2 - (Low p2,T,(m + 1)))) ; :: thesis:
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;
then (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 A24;
then consider s, t being Element of Bags n such that
A25: ( (HT (HM p2,T),T) + (HT red1,T) = s + t & s in Support (HM p1,T) & t in Support (red2 - (Low p2,T,(m + 1))) ) ;
A26: HT (HM p2,T),T = HT p2,T by TERMORD:26;
red1 <> 0_ n,L by POLYNOM7:def 2;
then Support red1 <> {} by POLYNOM7:1;
then A27: HT red1,T in Support red1 by TERMORD:def 6;
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 A28: s = HT p1,T by A25, TARSKI:def 1;
A29: red2 - (Low p2,T,(m + 1)) = red2 + (- (Low p2,T,(m + 1))) by POLYNOM1:def 23;
Support (- (Low p2,T,(m + 1))) = Support (Low p2,T,(m + 1)) by GROEB_1:5;
then A30: Support (red2 - (Low p2,T,(m + 1))) c= (Support red2) \/ (Support (Low p2,T,(m + 1))) by A29, POLYNOM1:79;
A31: Support (Low p2,T,(m + 1)) c= Support red2 by A11, A14, Th27;
t in Support red2

proof

now

per cases by A25, A30, 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 A31; :: thesis:

end;

hence t in Support red2 ; :: thesis:

end;

hence contradiction by A1, A25, A26, A27, A28, Th52; :: thesis:

end;

then ((HM p1,T) *' (red2 - (Low p2,T,(m + 1)))) . ((HT (HM p2,T),T) + (HT red1,T)) = 0. L by A18, POLYNOM1:def 9;
then A32: - (((HM p1,T) *' (red2 - (Low p2,T,(m + 1)))) . ((HT (HM p2,T),T) + (HT red1,T))) = 0. L by RLVECT_1:25;
A33: (HT (HM p2,T),T) + (HT red1,T) is Element of Bags n by POLYNOM1:def 14;
((((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 A23, 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 A32, 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 A17, A33, POLYNOM1:def 9;
then A34: (((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;
red2 <> 0_ n,L by POLYNOM7:def 2;
then A35: Support red2 <> {} by POLYNOM7:1;
A36: Support (Low p2,T,(m + 1)) = Lower_Support p2,T,(m + 1) by A11, Lm3;

now

assume A37: HT red2,T in Support (Low p2,T,(m + 1)) ; :: thesis:
Support (Low p2,T,(m + 1)) c= Support red2 by A11, A14, Th27;
then A38: for t being set st t in Support (Low p2,T,(m + 1)) holds
t in Support red2 ;

now

let t be set ; :: thesis:
assume A39: t in Support red2 ; :: thesis:
then reconsider t' = t as bag of by POLYNOM1:def 14;
A40: Support red2 c= Support p2 by TERMORD:35;
t' <= HT red2,T,T by A39, TERMORD:def 6;
hence t in Support (Low p2,T,(m + 1)) by A11, A36, A37, A39, A40, Th24; :: thesis:

end;

hence contradiction by A3, A7, A12, A38, TARSKI:2; :: thesis:

end;

then Low p2,T,(m + 1) <> red2 by A35, 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;
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 A41: Support z1 c= (Support (Red p2,T)) \/ (Support (Low p2,T,(m + 1))) by GROEB_1:5;
(Support (Red p2,T)) \/ (Support (Low p2,T,(m + 1))) c= (Support (Red p2,T)) \/ (Support (Red p2,T)) by A11, A14, Th27, XBOOLE_1:9;
then A42: Support z1 c= Support red2 by A41, XBOOLE_1:1;
reconsider z = (HM p1,T) *' z1 as non-zero Polynomial of n,L ;
z <> 0_ n,L by POLYNOM7:def 2;
then Support z <> {} by POLYNOM7:1;
then card (Support z) <> 0 ;
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;
A43: card (Support z) = card (Support z1) by Th10;
w = (card (Support z1)) - 1 by Th10;
then reconsider lowz1w = Low z1,T,w as non-zero Monomial of n,L by Th37;
set b = term lowzw;
A44: term lowzw is Element of Bags n by POLYNOM1:def 14;
set s = (term lowzw) / (HT p1,T);
A45: (term lowzw) / (HT p1,T) is Element of Bags n by POLYNOM1:def 14;
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));
A46: p1 <> 0_ n,L by POLYNOM7:def 2;
lowzw <> 0_ n,L by POLYNOM7:def 2;
then Support lowzw <> {} by POLYNOM7:1;
then Support lowzw = {(term lowzw)} by POLYNOM7:7;
then A47: term lowzw in Support lowzw by TARSKI:def 1;
card (Support z) = w + 1 ;
then A48: w < card (Support z) by NAT_1:16;
then A49: Support lowzw c= Support z by Th26;
then A50: term lowzw in Support ((HM p1,T) *' z1) by A47;
A51: ((HM p1,T) *' z1) . (term lowzw) <> 0. L by A47, A49, POLYNOM1:def 9;
Support ((HM p1,T) *' z1) c= { (t' + t) where t', t is Element of Bags n : ( t' in Support (HM p1,T) & t in Support z1 ) } by TERMORD:30;
then term lowzw in { (t' + t) where t', t is Element of Bags n : ( t' in Support (HM p1,T) & t in Support z1 ) } by A50;
then consider t', t being Element of Bags n such that
A52: ( term lowzw = t' + t & t' in Support (HM p1,T) & 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: t' = HT p1,T by A52, TARSKI:def 1;
then A54: HT p1,T divides term lowzw by A52, POLYNOM1:54;
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 POLYNOM1:52
.= t by A52, A53, A55, POLYNOM1:52 ;
then A57: (term lowzw) / (HT p1,T) in Support (Red p2,T) by A42, A52;
A58: Support (Red p2,T) c= Support p2 by TERMORD:35;
(term lowzw) / (HT p1,T) in (Support p2) \ {(HT p2,T)} by A57, 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 A57, A58, 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;

then A63: (Low p2,T,(m + 1)) . ((term lowzw) / (HT p1,T)) = 0. L by A45, POLYNOM1:def 9;

A64: now

assume A65: term lowzw in Support ((HM p2,T) *' (Red p1,T)) ; :: thesis:
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;
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 A65;
then consider t', t being Element of Bags n such that
A66: ( term lowzw = t' + t & t' in Support (HM p2,T) & t in Support (Red p1,T) ) ;
HM p2,T <> 0_ n,L by POLYNOM7:def 2;
then A67: Support (HM p2,T) <> {} by POLYNOM7:1;
then HT (HM p2,T),T in Support (HM p2,T) by TERMORD:def 6;
then A68: HT p2,T in Support (HM p2,T) by TERMORD:26;
consider x being bag of such that
A69: Support (HM p2,T) = {x} by A67, POLYNOM7:6;
Support (HM p2,T) = {(HT p2,T)} by A68, A69, TARSKI:def 1;
then t' = HT p2,T by A66, TARSKI:def 1;
hence contradiction by A1, A42, A52, A55, A56, A66, Th52; :: thesis:

end;

A70: now

assume ((Red p1,T) *' (Low p2,T,(m + 1))) . (term lowzw) <> 0. L ; :: thesis:
then A71: term lowzw in Support ((Red p1,T) *' (Low p2,T,(m + 1))) by A44, 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 A71;
then consider t', t being Element of Bags n such that
A72: ( term lowzw = t' + t & t' in Support (Red p1,T) & t in Support (Low p2,T,(m + 1)) ) ;
A73: ((term lowzw) / (HT p1,T)) + (HT p1,T) = t' + t by A54, A72, GROEB_2:def 1;
Support (Red p1,T) c= Support p1 by TERMORD:35;
then A74: t' <= HT p1,T,T by A72, TERMORD:def 6;
Support (Red p1,T) = (Support p1) \ {(HT p1,T)} by TERMORD:36;
then not t' in {(HT p1,T)} by A72, XBOOLE_0:def 5;
then t' <> HT p1,T by TARSKI:def 1;
then A75: t' < HT p1,T,T by A74, TERMORD:def 3;

now

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

end;

then t <= (term lowzw) / (HT p1,T),T by TERMORD:5;
then t + t' < ((term lowzw) / (HT p1,T)) + (HT p1,T),T by A75, Th6;
hence contradiction by A73, TERMORD:def 3; :: thesis:

end;

A77: ((((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 A70, 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 A44, A64, 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 ;

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 A77, RLVECT_1:30;
hence contradiction by A51, RLVECT_1:25; :: thesis:

end;

then 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 A44, 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))) 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 A34, A46, A55, POLYRED:def 5;
then A78: (((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 A78, 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 A79: 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;
p1 <> 0_ n,L by POLYNOM7:def 2;
then A80: HC p1,T <> 0. L by TERMORD:17;
((term lowzw) / (HT p1,T)) + (HT p1,T) = term ((HM p1,T) *' lowz1w) by A43, A48, A55, Th44
.= (term (HM p1,T)) + (term lowz1w) by Th7
.= (HT p1,T) + (term lowz1w) by TERMORD:22 ;
then A81: (term lowzw) / (HT p1,T) = ((HT p1,T) + (term lowz1w)) -' (HT p1,T) by POLYNOM1:52
.= term lowz1w by POLYNOM1:52 ;
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;
then (term lowzw) / (HT p1,T) in Support lowz1w by A81, TARSKI:def 1;
then A84: (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

A85: now

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

now

assume A87: 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, A84, A86, Th24;
then t in Support lowz1w by A82, Lm3;
then t = term lowz1w by A83, TARSKI:def 1;
hence contradiction by A81, A87, 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 A10, Th42;
then A88: HT (Low p2,T,m),T in (Support (Low p2,T,m)) \ (Support (Low p2,T,(m + 1))) by TARSKI:def 1;
then A89: HT (Low p2,T,m),T in Support (Low p2,T,m) by XBOOLE_0:def 5;
then A90: HT (Low p2,T,m),T in Lower_Support p2,T,m by A9, Lm3;
A91: Support (Low p2,T,m) c= Support p2 by A9, Th26;
A92: not HT (Low p2,T,m),T in Support (Low p2,T,(m + 1)) by A88, XBOOLE_0:def 5;

now

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

A94: now

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

end;

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

end;

then A96: 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 A97: HT (Low p2,T,m),T in Support red2 by A89, A91, A96, XBOOLE_0:def 5;
((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 A92, 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 ;
then z1 . (HT (Low p2,T,m),T) <> 0. L by A97, POLYNOM1:def 9;
then HT (Low p2,T,m),T in Support z1 by POLYNOM1:def 9;
then A98: (term lowzw) / (HT p1,T) <= HT (Low p2,T,m),T,T by A85;
Support red2 c= Support p2 by TERMORD:35;
then (term lowzw) / (HT p1,T) in Lower_Support p2,T,m by A9, A57, A90, A98, Th24;
then A99: (term lowzw) / (HT p1,T) in Support (Low p2,T,m) by A9, 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 A10, Th42;
then A100: (term lowzw) / (HT p1,T) = HT (Low p2,T,m),T by TARSKI:def 1;
then A101: (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 A9, A99, 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 A101, TERMORD:18 ;
hence Monom (p2 . ((term lowzw) / (HT p1,T))),((term lowzw) / (HT p1,T)) = HM (Low p2,T,m),T by A100, TERMORD:def 8; :: thesis:

end;

then A102: 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 A10, Th43 ;
A103: HT p1,T = HT (HM p1,T),T by TERMORD:26
.= term (HM p1,T) by TERMORD: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)))) . (term lowzw) = - ((HC p1,T) * (p2 . ((term lowzw) / (HT p1,T))))

proof

((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 A103, 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 A57, A58, 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 A63, RLVECT_1:25
.= (HC p1,T) * (p2 . ((term lowzw) / (HT p1,T))) by RLVECT_1:def 7 ;
hence ((((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) * (p2 . ((term lowzw) / (HT p1,T)))) by A77; :: thesis:

end;

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 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 A80, VECTSP_1:def 22
.= (- (p2 . ((term lowzw) / (HT p1,T)))) * (((term lowzw) / (HT p1,T)) *' p1) by VECTSP_1:def 16 ;
then A104: ((((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 A102, 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 A102, 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 ;
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 A8, A13;
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 A79, A104, REWRITE1:17; :: thesis:

end;

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

end;

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

end;

A105: for i being Element of NAT st 0 <= i & i <= j' holds
S₁[i] from POLYNOM2:sch 4(A5, A6);
A106: card (Support (Low p2,T,1)) = j' by A3, Th36;
(((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 ;
hence PolyRedRel {p1},T reduces ((HM p2,T) *' (Red p1,T)) - ((HM p1,T) *' (Red p2,T)),p2 *' (Red p1,T) by A4, A105, A106; :: thesis: