let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p1, p2 being non-zero Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint & Red (p1,T) is non-zero & Red (p2,T) is non-zero holds
PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),p2 *' (Red (p1,T))
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p1, p2 being non-zero Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint & Red (p1,T) is non-zero & Red (p2,T) is non-zero holds
PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),p2 *' (Red (p1,T))
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p1, p2 being non-zero Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint & Red (p1,T) is non-zero & Red (p2,T) is non-zero holds
PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),p2 *' (Red (p1,T))
let p1, p2 be non-zero Polynomial of n,L; :: thesis: ( HT (p1,T), HT (p2,T) are_disjoint & Red (p1,T) is non-zero & Red (p2,T) is non-zero implies PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),p2 *' (Red (p1,T)) )
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: PolyRedRel ({p1},T) reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),p2 *' (Red (p1,T))
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₁[ 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)));

now :: thesis: not card (Support p2) = 0

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

end;

then A3: 1 <= card (Support p2) by NAT_1:14;
then 1 - 1 <= (card (Support p2)) - 1 by XREAL_1:9;
then reconsider j9 = (card (Support p2)) - 1 as Element of NAT by INT_1:3;
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:24
.= (((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:26
.= p2 *' (Red (p1,T)) by TERMORD:38 ;
p2 <> 0_ (n,L) by POLYNOM7:def 1;
then Support p2 <> {} by POLYNOM7:1;
then HT (p2,T) in Support p2 by TERMORD:def 6;
then for t being object st t in {(HT (p2,T))} holds
t in Support p2 by TARSKI:def 1;
then A5: {(HT (p2,T))} c= Support p2 ;
A6: card (Support red2) = card ((Support p2) \ {(HT (p2,T))}) by TERMORD:36
.= (card (Support p2)) - (card {(HT (p2,T))}) by A5, CARD_2:44
.= (card (Support p2)) - 1 by CARD_2:42 ;
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: ( 0 <= k & k < j9 & S₁[k] implies S₁[k + 1] )
assume that
0 <= k and
A9: k < j9 ; :: thesis: ( not S₁[k] or S₁[k + 1] )

now :: thesis: ( S₁[k] implies S₁[k + 1] )

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

now :: thesis: for m being Element of NAT st m <= card (Support p2) & card (Support (Low (p2,T,m))) = k + 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)))

( 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 A11: ((HM (p2,T)) *' red1) . ((HT ((HM (p2,T)),T)) + (HT (red1,T))) <> 0. L by TERMORD:def 7;
A12: Support (Red (p2,T)) c= Support p2 by TERMORD:35;
red2 <> 0_ (n,L) by POLYNOM7:def 1;
then A13: Support red2 <> {} by POLYNOM7:1;
let m be Element of NAT ; :: thesis: ( m <= card (Support p2) & card (Support (Low (p2,T,m))) = k + 1 implies 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 that
A14: m <= card (Support p2) and
A15: card (Support (Low (p2,T,m))) = k + 1 ; :: thesis: 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)))
set m9 = m + 1;

now :: thesis: not m = card (Support p2)

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

end;

then A16: m < card (Support p2) by A14, 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:44;
then A17: (k + 1) - (card (Support (Low (p2,T,(m + 1))))) = card {(HT ((Low (p2,T,m)),T))} by A15, A16, Th42
.= 1 by CARD_1:30 ;
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))));
A18: (HT ((HM (p2,T)),T)) + (HT (red1,T)) is Element of Bags n by PRE_POLY:def 12;
A19: m + 1 <= card (Support p2) by A16, NAT_1:13;

now :: thesis: not (HT ((HM (p2,T)),T)) + (HT (red1,T)) in Support (red1 *' (Low (p2,T,(m + 1))))

A20: 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: contradiction
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 A20;
then consider s, t being Element of Bags n such that
A21: (HT ((HM (p2,T)),T)) + (HT (red1,T)) = s + t and
A22: s in Support red1 and
A23: t in Support (Low (p2,T,(m + 1))) ;
A24: t < HT (p2,T),T

proof

now :: thesis: ( ( m + 1 = card (Support p2) & contradiction ) or ( m + 1 <> card (Support p2) & t < HT (p2,T),T ) )

per cases ( m + 1 = card (Support p2) or m + 1 <> card (Support p2) ) ;

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

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

end;

case A25: m + 1 <> card (Support p2) ; :: thesis: t < HT (p2,T),T

A26: t <= HT ((Low (p2,T,(m + 1))),T),T by A23, TERMORD:def 6;
m + 1 < card (Support p2) by A19, A25, XXREAL_0:1;
hence t < HT (p2,T),T by A26, Th3, Th39; :: thesis: verum

end;

end;

end;

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

end;

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

end;

then A27: (red1 *' (Low (p2,T,(m + 1)))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T))) = 0. L by A18, POLYNOM1:def 4;
A28: 1 <= m + 1 by NAT_1:14;

now :: thesis: not (HT ((HM (p2,T)),T)) + (HT (red1,T)) in Support ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1)))))

red1 <> 0_ (n,L) by POLYNOM7:def 1;
then Support red1 <> {} by POLYNOM7:1;
then A29: ( HT ((HM (p2,T)),T) = HT (p2,T) & HT (red1,T) in Support red1 ) by TERMORD:26, TERMORD:def 6;
A30: 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: contradiction
then A31: (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 A30;
( 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 7;
then A32: Support (red2 - (Low (p2,T,(m + 1)))) c= (Support red2) \/ (Support (Low (p2,T,(m + 1)))) by POLYNOM1:20;
consider s, t being Element of Bags n such that
A33: (HT ((HM (p2,T)),T)) + (HT (red1,T)) = s + t and
A34: s in Support (HM (p1,T)) and
A35: t in Support (red2 - (Low (p2,T,(m + 1)))) by A31;
A36: Support (Low (p2,T,(m + 1))) c= Support red2 by A19, A28, Th27;
A37: t in Support red2

proof

now :: thesis: ( ( t in Support red2 & t in Support red2 ) or ( t in Support (Low (p2,T,(m + 1))) & t in Support red2 ) )

per cases ( t in Support red2 or t in Support (Low (p2,T,(m + 1))) ) by A35, A32, XBOOLE_0:def 3;

case t in Support red2 ; :: thesis: t in Support red2

hence t in Support red2 ; :: thesis: verum

end;

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

hence t in Support red2 by A36; :: thesis: verum

end;

end;

end;

hence t in Support red2 ; :: thesis: verum

end;

HM (p1,T) <> 0_ (n,L) by POLYNOM7:def 1;
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 A34, TARSKI:def 1;
hence contradiction by A1, A33, A29, A37, Th52; :: thesis: verum

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 4;
then A38: - (((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T)))) = 0. L by RLVECT_1:12;
A39: Support (Low (p2,T,(m + 1))) = Lower_Support (p2,T,(m + 1)) by A19, Lm3;

now :: thesis: not HT (red2,T) in Support (Low (p2,T,(m + 1)))

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

A41: now :: thesis: for t being object st t in Support red2 holds
t in Support (Low (p2,T,(m + 1)))

let t be object ; :: thesis: ( t in Support red2 implies t in Support (Low (p2,T,(m + 1))) )
assume A42: t in Support red2 ; :: thesis: t in Support (Low (p2,T,(m + 1)))
then reconsider t9 = t as bag of n ;
( Support red2 c= Support p2 & t9 <= HT (red2,T),T ) by A42, TERMORD:35, TERMORD:def 6;
hence t in Support (Low (p2,T,(m + 1))) by A19, A39, A40, A42, Th24; :: thesis: verum

end;

Support (Low (p2,T,(m + 1))) c= Support red2 by A19, A28, Th27;
then for t being object st t in Support (Low (p2,T,(m + 1))) holds
t in Support red2 ;
hence contradiction by A6, A9, A17, A41, TARSKI:2; :: thesis: verum

end;

then Low (p2,T,(m + 1)) <> red2 by A13, 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 1;
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 7;
then Support z1 c= (Support (Red (p2,T))) \/ (Support (- (Low (p2,T,(m + 1))))) by POLYNOM1:20;
then A43: Support z1 c= (Support (Red (p2,T))) \/ (Support (Low (p2,T,(m + 1)))) by GROEB_1:5;
z <> 0_ (n,L) by POLYNOM7:def 1;
then Support z <> {} by POLYNOM7:1;
then reconsider w = (card (Support z)) - 1 as Element of NAT by INT_1:5, 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));
A44: 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 A45: w < card (Support z) by NAT_1:16;
then A46: Support lowzw c= Support z by Th26;
lowzw <> 0_ (n,L) by POLYNOM7:def 1;
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;
then term lowzw in Support ((HM (p1,T)) *' z1) by A46;
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 A44;
then consider t9, t being Element of Bags n such that
A48: term lowzw = t9 + t and
A49: t9 in Support (HM (p1,T)) and
A50: t in Support z1 ;
HM (p1,T) <> 0_ (n,L) by POLYNOM7:def 1;
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 A51: t9 = HT (p1,T) by A49, TARSKI:def 1;
then A52: HT (p1,T) divides term lowzw by A48, PRE_POLY:50;
then A53: ((term lowzw) / (HT (p1,T))) + (HT (p1,T)) = term lowzw by GROEB_2:def 1;
A54: (term lowzw) / (HT (p1,T)) = (((term lowzw) / (HT (p1,T))) + (HT (p1,T))) -' (HT (p1,T)) by PRE_POLY:48
.= t by A48, A51, A53, PRE_POLY:48 ;
(Support (Red (p2,T))) \/ (Support (Low (p2,T,(m + 1)))) c= (Support (Red (p2,T))) \/ (Support (Red (p2,T))) by A19, A28, Th27, XBOOLE_1:9;
then A55: Support z1 c= Support red2 by A43;
then A56: (term lowzw) / (HT (p1,T)) in Support (Red (p2,T)) by A50, A54;
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 A57: (term lowzw) / (HT (p1,T)) <> HT (p2,T) by TARSKI:def 1;
then A58: (Red (p2,T)) . ((term lowzw) / (HT (p1,T))) = p2 . ((term lowzw) / (HT (p1,T))) by A56, A12, TERMORD:40;

A59: now :: thesis: not (term lowzw) / (HT (p1,T)) in Support (Low (p2,T,(m + 1)))

assume (term lowzw) / (HT (p1,T)) in Support (Low (p2,T,(m + 1))) ; :: thesis: contradiction
then A60: 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 7
.= ((Red (p2,T)) . ((term lowzw) / (HT (p1,T)))) + ((- (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T)))) by POLYNOM1:15
.= ((Red (p2,T)) . ((term lowzw) / (HT (p1,T)))) + (- ((Low (p2,T,(m + 1))) . ((term lowzw) / (HT (p1,T))))) by POLYNOM1:17
.= 0. L by A58, A60, RLVECT_1:5 ;
hence contradiction by A50, A54, POLYNOM1:def 4; :: thesis: verum

end;

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

A62: now :: thesis: not ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) . (term lowzw) <> 0. L

assume ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) . (term lowzw) <> 0. L ; :: thesis: contradiction
then A63: term lowzw in Support ((Red (p1,T)) *' (Low (p2,T,(m + 1)))) by A61, POLYNOM1:def 4;
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 A63;
then consider t9, t being Element of Bags n such that
A64: term lowzw = t9 + t and
A65: t9 in Support (Red (p1,T)) and
A66: t in Support (Low (p2,T,(m + 1))) ;
A67: ((term lowzw) / (HT (p1,T))) + (HT (p1,T)) = t9 + t by A52, A64, GROEB_2:def 1;

now :: thesis: not (term lowzw) / (HT (p1,T)) < t,T

assume (term lowzw) / (HT (p1,T)) < t,T ; :: thesis: contradiction
then A68: (term lowzw) / (HT (p1,T)) <= t,T by TERMORD:def 3;
t in Lower_Support (p2,T,(m + 1)) by A19, A66, Lm3;
then (term lowzw) / (HT (p1,T)) in Lower_Support (p2,T,(m + 1)) by A19, A56, A12, A68, Th24;
hence contradiction by A19, A59, Lm3; :: thesis: verum

end;

then A69: 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 A65, XBOOLE_0:def 5;
then A70: 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 A65, TERMORD:def 6;
then t9 < HT (p1,T),T by A70, TERMORD:def 3;
then t + t9 < ((term lowzw) / (HT (p1,T))) + (HT (p1,T)),T by A69, Th6;
hence contradiction by A67, TERMORD:def 3; :: thesis: verum

end;

A71: now :: thesis: not term lowzw in Support ((HM (p2,T)) *' (Red (p1,T)))

HM (p2,T) <> 0_ (n,L) by POLYNOM7:def 1;
then A72: Support (HM (p2,T)) <> {} by POLYNOM7:1;
then HT ((HM (p2,T)),T) in Support (HM (p2,T)) by TERMORD:def 6;
then A73: HT (p2,T) in Support (HM (p2,T)) by TERMORD:26;
A74: 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: contradiction
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 A74;
then consider t9, t being Element of Bags n such that
A75: term lowzw = t9 + t and
A76: t9 in Support (HM (p2,T)) and
A77: t in Support (Red (p1,T)) ;
ex x being bag of n st Support (HM (p2,T)) = {x} by A72, POLYNOM7:6;
then Support (HM (p2,T)) = {(HT (p2,T))} by A73, TARSKI:def 1;
then t9 = HT (p2,T) by A76, TARSKI:def 1;
hence contradiction by A1, A55, A50, A53, A54, A75, A77, Th52; :: thesis: verum

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));
A78: (HT ((HM (p2,T)),T)) + (HT (red1,T)) is Element of Bags n by PRE_POLY:def 12;
A79: ((((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 7
.= ((((HM (p2,T)) *' red1) + (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))))) . (term lowzw)) + (0. L) by A62, POLYNOM1:15
.= (((HM (p2,T)) *' red1) + (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))))) . (term lowzw) by RLVECT_1:def 4
.= (((HM (p2,T)) *' red1) . (term lowzw)) + ((- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1)))))) . (term lowzw)) by POLYNOM1:15
.= (0. L) + ((- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1)))))) . (term lowzw)) by A61, A71, POLYNOM1:def 4
.= (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1)))))) . (term lowzw) by RLVECT_1:def 4
.= - (((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))) . (term lowzw)) by POLYNOM1:17 ;
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 A80: w <= card (Support z1) by NAT_1:13;
lowz1w <> 0_ (n,L) by POLYNOM7:def 1;
then Support lowz1w <> {} by POLYNOM7:1;
then A81: 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 A45, A53, Th44
.= (term (HM (p1,T))) + (term lowz1w) by Th7
.= (HT (p1,T)) + (term lowz1w) by TERMORD:22 ;
then A82: (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 A81, TARSKI:def 1;
then A83: (term lowzw) / (HT (p1,T)) in Lower_Support (z1,T,w) by A80, Lm3;
Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T)))) = HM ((Low (p2,T,m)),T)

proof

A84: now :: thesis: for t being bag of n st t in Support z1 holds
(term lowzw) / (HT (p1,T)) <= t,T

let t be bag of n; :: thesis: ( t in Support z1 implies (term lowzw) / (HT (p1,T)) <= t,T )
assume A85: t in Support z1 ; :: thesis: (term lowzw) / (HT (p1,T)) <= t,T

now :: thesis: not t < (term lowzw) / (HT (p1,T)),T

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

end;

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

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 A16, Th42;
then A87: HT ((Low (p2,T,m)),T) in (Support (Low (p2,T,m))) \ (Support (Low (p2,T,(m + 1)))) by TARSKI:def 1;
then A88: not HT ((Low (p2,T,m)),T) in Support (Low (p2,T,(m + 1))) by XBOOLE_0:def 5;
A89: ((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 7
.= ((Red (p2,T)) . (HT ((Low (p2,T,m)),T))) + ((- (Low (p2,T,(m + 1)))) . (HT ((Low (p2,T,m)),T))) by POLYNOM1:15
.= ((Red (p2,T)) . (HT ((Low (p2,T,m)),T))) + (- ((Low (p2,T,(m + 1))) . (HT ((Low (p2,T,m)),T)))) by POLYNOM1:17
.= ((Red (p2,T)) . (HT ((Low (p2,T,m)),T))) + (- (0. L)) by A88, POLYNOM1:def 4
.= ((Red (p2,T)) . (HT ((Low (p2,T,m)),T))) + (0. L) by RLVECT_1:12
.= (Red (p2,T)) . (HT ((Low (p2,T,m)),T)) by RLVECT_1:def 4 ;
A90: HT ((Low (p2,T,m)),T) in Support (Low (p2,T,m)) by A87, XBOOLE_0:def 5;
then A91: HT ((Low (p2,T,m)),T) in Lower_Support (p2,T,m) by A14, Lm3;
A92: Support (Low (p2,T,m)) c= Support p2 by A14, Th26;

now :: thesis: not HT ((Low (p2,T,m)),T) = HT (p2,T)

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

A94: now :: thesis: for u being object st u in Support p2 holds
u in Support (Low (p2,T,m))

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

end;

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

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 HT ((Low (p2,T,m)),T) in Support red2 by A90, A92, A96, XBOOLE_0:def 5;
then z1 . (HT ((Low (p2,T,m)),T)) <> 0. L by A89, POLYNOM1:def 4;
then A97: HT ((Low (p2,T,m)),T) in Support z1 by POLYNOM1:def 4;
Support red2 c= Support p2 by TERMORD:35;
then (term lowzw) / (HT (p1,T)) in Lower_Support (p2,T,m) by A14, A56, A84, A91, A97, Th24;
then A98: (term lowzw) / (HT (p1,T)) in Support (Low (p2,T,m)) by A14, Lm3;
then (term lowzw) / (HT (p1,T)) in (Support (Low (p2,T,m))) \ (Support (Low (p2,T,(m + 1)))) by A59, XBOOLE_0:def 5;
then (term lowzw) / (HT (p1,T)) in {(HT ((Low (p2,T,m)),T))} by A16, Th42;
then A99: (term lowzw) / (HT (p1,T)) = HT ((Low (p2,T,m)),T) by TARSKI:def 1;
then A100: (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 A14, A98, 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 A100, TERMORD:18 ;
hence Monom ((p2 . ((term lowzw) / (HT (p1,T)))),((term lowzw) / (HT (p1,T)))) = HM ((Low (p2,T,m)),T) by A99, TERMORD:def 8; :: thesis: verum

end;

then A101: 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 A16, Th43 ;
A102: ((HM (p1,T)) *' z1) . (term lowzw) <> 0. L by A47, A46, POLYNOM1:def 4;

now :: thesis: not ((((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

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: contradiction
then ((HM (p1,T)) *' z1) . (term lowzw) = - (0. L) by A79, RLVECT_1:17;
hence contradiction by A102, RLVECT_1:12; :: thesis: verum

end;

then A103: ( 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 A61, POLYNOM1:def 4, POLYNOM7:def 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))))) . ((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 7
.= ((((HM (p2,T)) *' red1) + (- ((HM (p1,T)) *' (red2 - (Low (p2,T,(m + 1))))))) . ((HT ((HM (p2,T)),T)) + (HT (red1,T)))) + (0. L) by A27, POLYNOM1:15
.= (((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 4
.= (((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:15
.= (((HM (p2,T)) *' red1) . ((HT ((HM (p2,T)),T)) + (HT (red1,T)))) + (0. L) by A38, POLYNOM1:17
.= ((HM (p2,T)) *' red1) . ((HT ((HM (p2,T)),T)) + (HT (red1,T))) by RLVECT_1:def 4 ;
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 A11, A78, POLYNOM1:def 4;
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 A53, A103, POLYRED:def 5;
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)))) 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 A104, 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 A105: 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:15;
m + 1 <= card (Support p2) by A16, NAT_1:13;
then A106: 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, A17;
A107: 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 A108: (Low (p2,T,(m + 1))) . ((term lowzw) / (HT (p1,T))) = 0. L by A59, POLYNOM1:def 4;
A109: Low (p2,T,m) = - (- (Low (p2,T,m))) by POLYNOM1:19;
A110: Low (p2,T,(m + 1)) = - (- (Low (p2,T,(m + 1)))) by POLYNOM1:19;
((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 A52, GROEB_2:def 1
.= ((HM (p1,T)) . (HT (p1,T))) * ((red2 - (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T)))) by A107, 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 7
.= (HC (p1,T)) * ((red2 . ((term lowzw) / (HT (p1,T)))) + ((- (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T))))) by POLYNOM1:15
.= (HC (p1,T)) * ((p2 . ((term lowzw) / (HT (p1,T)))) + ((- (Low (p2,T,(m + 1)))) . ((term lowzw) / (HT (p1,T))))) by A56, A12, A57, TERMORD:40
.= (HC (p1,T)) * ((p2 . ((term lowzw) / (HT (p1,T)))) + (- ((Low (p2,T,(m + 1))) . ((term lowzw) / (HT (p1,T)))))) by POLYNOM1:17
.= (HC (p1,T)) * ((p2 . ((term lowzw) / (HT (p1,T)))) + (0. L)) by A108, RLVECT_1:12
.= (HC (p1,T)) * (p2 . ((term lowzw) / (HT (p1,T)))) by RLVECT_1:def 4 ;
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 A79, VECTSP_1:9
.= (((HC (p1,T)) * (- (p2 . ((term lowzw) / (HT (p1,T)))))) * ((HC (p1,T)) ")) * (((term lowzw) / (HT (p1,T))) *' p1)
.= ((- (p2 . ((term lowzw) / (HT (p1,T))))) * ((HC (p1,T)) * ((HC (p1,T)) "))) * (((term lowzw) / (HT (p1,T))) *' p1) by GROUP_1:def 3
.= ((- (p2 . ((term lowzw) / (HT (p1,T))))) * (1. L)) * (((term lowzw) / (HT (p1,T))) *' p1) by VECTSP_1:def 10
.= (- (p2 . ((term lowzw) / (HT (p1,T))))) * (((term lowzw) / (HT (p1,T))) *' p1) ;
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 7
.= ((((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:17
.= ((((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:26
.= ((((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 7
.= (((((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:21
.= (((((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:21
.= (((((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:21
.= ((((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:26
.= (((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:21
.= (((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 A101, POLYNOM1:26
.= (((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 7
.= (((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 A109, A110, A101, POLYNOM1:21
.= (((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 7
.= (((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 7 ;
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 A105, A106, REWRITE1:16; :: thesis: verum

end;

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

end;

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

end;

A111: S₁[ 0 ]

proof

let m be Element of NAT ; :: thesis: ( m <= card (Support p2) & card (Support (Low (p2,T,m))) = 0 implies 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 that
m <= card (Support p2) and
A112: card (Support (Low (p2,T,m))) = 0 ; :: thesis: 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)))
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:12; :: thesis: verum

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: verum