let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
g < f,T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
g < f,T
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
g < f,T
let f, p, g be Polynomial of n,L; :: thesis: ( f reduces_to g,p,T implies g < f,T )
set R = RelStr(# (Bags n),T #);
defpred S₁[ Nat] means for f, p, g being Polynomial of n,L st card (Support f) = $1 & f reduces_to g,p,T holds
[(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #);
A1: ex k being Nat st card (Support f) = k ;
assume A2: f reduces_to g,p,T ; :: thesis: g < f,T
then consider b being bag of n such that
A3: f reduces_to g,p,b,T ;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: for f, p, g being Polynomial of n,L st card (Support f) = k & f reduces_to g,p,T holds
[(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: S₁[k + 1]

now :: thesis: for f, p, g being Polynomial of n,L st card (Support f) = k + 1 & f reduces_to g,p,T holds
[(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

A6: T is_connected_in field T by RELAT_2:def 14;
let f, p, g be Polynomial of n,L; :: thesis: ( card (Support f) = k + 1 & f reduces_to g,p,T implies [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) )
assume that
A7: card (Support f) = k + 1 and
A8: f reduces_to g,p,T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)
consider b being bag of n such that
A9: f reduces_to g,p,b,T by A8;
consider s being bag of n such that
A10: s + (HT (p,T)) = b and
A11: g = f - (((f . b) / (HC (p,T))) * (s *' p)) by A9;
A12: b in Support f by A9;
A13: f <> 0_ (n,L) by A9;

now :: thesis: ( ( HT (f,T) <> HT (g,T) & [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ) or ( HT (g,T) = HT (f,T) & [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ) )

per cases ( HT (f,T) <> HT (g,T) or HT (g,T) = HT (f,T) ) ;

case A14: HT (f,T) <> HT (g,T) ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

HT (g,T) <= HT (g,T),T by TERMORD:6;
then [(HT (g,T)),(HT (g,T))] in T by TERMORD:def 2;
then A15: HT (g,T) in field T by RELAT_1:15;
HT (f,T) <= HT (f,T),T by TERMORD:6;
then [(HT (f,T)),(HT (f,T))] in T by TERMORD:def 2;
then HT (f,T) in field T by RELAT_1:15;
then A16: ( [(HT (f,T)),(HT (g,T))] in T or [(HT (g,T)),(HT (f,T))] in T ) by A6, A14, A15, RELAT_2:def 6;

now :: thesis: ( ( HT (f,T) <= HT (g,T),T & [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ) or ( HT (g,T) <= HT (f,T),T & [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ) )

per cases ( HT (f,T) <= HT (g,T),T or HT (g,T) <= HT (f,T),T ) by A16, TERMORD:def 2;

case A17: HT (f,T) <= HT (g,T),T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

now :: thesis: HT (g,T) in Support g

assume not HT (g,T) in Support g ; :: thesis: contradiction
then HT (g,T) = EmptyBag n by TERMORD:def 6;
then [(HT (g,T)),(HT (f,T))] in T by BAGORDER:def 5;
then HT (g,T) <= HT (f,T),T by TERMORD:def 2;
hence contradiction by A14, A17, TERMORD:7; :: thesis: verum

end;

then HT (g,T) <= HT (f,T),T by A8, Th42;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by A14, A17, TERMORD:7; :: thesis: verum

end;

case HT (g,T) <= HT (f,T),T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

then HT (g,T) < HT (f,T),T by A14, TERMORD:def 3;
then g < f,T by Lm15;
then g <= f,T ;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: verum

end;

end;

end;

hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: verum

end;

case A18: HT (g,T) = HT (f,T) ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

now :: thesis: ( ( b = HT (f,T) & [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ) or ( b <> HT (f,T) & [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ) )

per cases ( b = HT (f,T) or b <> HT (f,T) ) ;

case b = HT (f,T) ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

then not HT (g,T) in Support g by A9, A18, Lm17;
then Support g = {} by TERMORD:def 6;
then g = 0_ (n,L) by POLYNOM7:1;
then g <= f,T by Lm12;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: verum

end;

case A19: b <> HT (f,T) ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)

HT (f,T) in Support f by A12, TERMORD:def 6;
then for u being object st u in {(HT (f,T))} holds
u in Support f by TARSKI:def 1;
then A20: {(HT (f,T))} c= Support f by TARSKI:def 3;
A21: Support (Red (f,T)) = (Support f) \ {(HT (f,T))} by TERMORD:36;
not b in {(HT (f,T))} by A19, TARSKI:def 1;
then A22: b in Support (Red (f,T)) by A12, A21, XBOOLE_0:def 5;
then Red (f,T) <> 0_ (n,L) by POLYNOM7:1;
then reconsider rf = Red (f,T) as non-zero Polynomial of n,L by POLYNOM7:def 1;
A23: ( rf <> 0_ (n,L) & p <> 0_ (n,L) ) by A9, POLYNOM7:def 1;
b <= HT (f,T),T by A12, TERMORD:def 6;
then b < HT (f,T),T by A19, TERMORD:def 3;
then f . (HT (f,T)) = g . (HT (g,T)) by A9, A18, Th41;
then HC (f,T) = g . (HT (g,T)) by TERMORD:def 7
.= HC (g,T) by TERMORD:def 7 ;
then HM (f,T) = Monom ((HC (g,T)),(HT (g,T))) by A18, TERMORD:def 8
.= HM (g,T) by TERMORD:def 8 ;
then Red (g,T) = (f - (((f . b) / (HC (p,T))) * (s *' p))) - (HM (f,T)) by A11, TERMORD:def 9
.= (((HM (f,T)) + rf) - (((f . b) / (HC (p,T))) * (s *' p))) - (HM (f,T)) by TERMORD:38
.= (((HM (f,T)) + rf) - (((rf . b) / (HC (p,T))) * (s *' p))) - (HM (f,T)) by A12, A19, TERMORD:40
.= (((HM (f,T)) + rf) + (- (((rf . b) / (HC (p,T))) * (s *' p)))) - (HM (f,T)) by POLYNOM1:def 7
.= ((HM (f,T)) + (rf + (- (((rf . b) / (HC (p,T))) * (s *' p))))) - (HM (f,T)) by POLYNOM1:21
.= ((HM (f,T)) + (rf + (- (((rf . b) / (HC (p,T))) * (s *' p))))) + (- (HM (f,T))) by POLYNOM1:def 7
.= (rf + (- (((rf . b) / (HC (p,T))) * (s *' p)))) + ((HM (f,T)) + (- (HM (f,T)))) by POLYNOM1:21
.= (rf - (((rf . b) / (HC (p,T))) * (s *' p))) + ((HM (f,T)) + (- (HM (f,T)))) by POLYNOM1:def 7
.= (rf - (((rf . b) / (HC (p,T))) * (s *' p))) + ((HM (f,T)) - (HM (f,T))) by POLYNOM1:def 7
.= (rf - (((rf . b) / (HC (p,T))) * (s *' p))) + (0_ (n,L)) by POLYNOM1:24
.= rf - (((rf . b) / (HC (p,T))) * (s *' p)) by POLYNOM1:23 ;
then rf reduces_to Red (g,T),p,b,T by A10, A22, A23;
then A24: rf reduces_to Red (g,T),p,T ;
HT (f,T) in {(HT (f,T))} by TARSKI:def 1;
then A25: not HT (f,T) in Support (Red (f,T)) by A21, XBOOLE_0:def 5;
(Support (Red (f,T))) \/ {(HT (f,T))} = (Support f) \/ {(HT (f,T))} by A21, XBOOLE_1:39
.= Support f by A20, XBOOLE_1:12 ;
then (card (Support (Red (f,T)))) + 1 = k + 1 by A7, A25, CARD_2:41;
then [(Support (Red (g,T))),(Support rf)] in FinOrd RelStr(# (Bags n),T #) by A5, A24, XCMPLX_1:2;
then Red (g,T) <= Red (f,T),T ;
then g <= f,T by A13, A18, Lm16;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: verum

end;

end;

end;

hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: verum

end;

end;

end;

hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) ; :: thesis: verum

end;

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

end;

A26: S₁[ 0 ]

proof

let f, p, g be Polynomial of n,L; :: thesis: ( card (Support f) = 0 & f reduces_to g,p,T implies [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) )
assume that
A27: card (Support f) = 0 and
A28: f reduces_to g,p,T ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)
Support f = {} by A27;
then f = 0_ (n,L) by POLYNOM7:1;
then f is_irreducible_wrt p,T by Th37;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by A28; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A26, A4);
then [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by A2, A1;
then A29: g <= f,T ;
Support f <> Support g by A3, Lm17;
hence g < f,T by A29; :: thesis: verum