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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 #);
assume A1: f reduces_to g,p,T ; :: thesis: g < f,T
then consider b being bag of such that
A2: f reduces_to g,p,b,T by Def6;
b in Support f by A2, Def5;
then A3: Support f <> Support g by A2, Lm17;
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 #);
A4: 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 A5: ( card (Support f) = 0 & f reduces_to g,p,T ) ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)
then Support f, {} are_equipotent by CARD_1:def 5;
then Support f = {} by CARD_1:46;
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 A5, Def8; :: thesis: verum

end;

A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: 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

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 A8: ( card (Support f) = k + 1 & f reduces_to g,p,T ) ; :: thesis: [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #)
then consider b being bag of such that
A9: f reduces_to g,p,b,T by Def6;
consider s being bag of such that
A10: ( s + (HT p,T) = b & g = f - (((f . b) / (HC p,T)) * (s *' p)) ) by A9, Def5;
A11: b in Support f by A9, Def5;
A12: T is_connected_in field T by RELAT_2:def 14;
A13: f <> 0_ n,L by A9, Def5;

now

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 f,T <= HT f,T,T & HT g,T <= HT g,T,T ) by TERMORD:6;
then ( [(HT f,T),(HT f,T)] in T & [(HT g,T),(HT g,T)] in T ) by TERMORD:def 2;
then ( HT f,T in field T & HT g,T in field T ) by RELAT_1:30;
then A15: ( [(HT f,T),(HT g,T)] in T or [(HT g,T),(HT f,T)] in T ) by A12, A14, RELAT_2:def 6;

now

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

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

now

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 7;
then HT g,T <= HT f,T,T by TERMORD:def 2;
hence contradiction by A14, A16, 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, A16, 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 by Def3;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by Def2; :: thesis: verum

end;

end;

end;

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

end;

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

now

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, A17, 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 #) by Def2; :: thesis: verum

end;

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

b <= HT f,T,T by A11, TERMORD:def 6;
then b < HT f,T,T by A18, TERMORD:def 3;
then f . (HT f,T) = g . (HT g,T) by A9, A17, Th41;
then HC f,T = g . (HT g,T) by TERMORD:def 7
.= HC g,T by TERMORD:def 7 ;
then A19: HM f,T = Monom (HC g,T),(HT g,T) by A17, TERMORD:def 8
.= HM g,T by TERMORD:def 8 ;
A20: not b in {(HT f,T)} by A18, TARSKI:def 1;
A21: Support (Red f,T) = (Support f) \ {(HT f,T)} by TERMORD:36;
then A22: b in Support (Red f,T) by A11, A20, 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 2;
HT f,T in Support f by A11, TERMORD:def 6;
then for u being set st u in {(HT f,T)} holds
u in Support f by TARSKI:def 1;
then A23: {(HT f,T)} c= Support f by TARSKI:def 3;
A24: (Support (Red f,T)) \/ {(HT f,T)} = (Support f) \/ {(HT f,T)} by A21, XBOOLE_1:39
.= Support f by A23, XBOOLE_1:12 ;
HT f,T in {(HT f,T)} by TARSKI:def 1;
then not HT f,T in Support (Red f,T) by A21, XBOOLE_0:def 5;
then A25: (card (Support (Red f,T))) + 1 = k + 1 by A8, A24, CARD_2:54;
A26: ( rf <> 0_ n,L & p <> 0_ n,L ) by A9, Def5, POLYNOM7:def 2;
Red g,T = (f - (((f . b) / (HC p,T)) * (s *' p))) - (HM f,T) by A10, A19, 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 A11, A18, TERMORD:40
.= (((HM f,T) + rf) + (- (((rf . b) / (HC p,T)) * (s *' p)))) - (HM f,T) by POLYNOM1:def 23
.= ((HM f,T) + (rf + (- (((rf . b) / (HC p,T)) * (s *' p))))) - (HM f,T) by POLYNOM1:80
.= ((HM f,T) + (rf + (- (((rf . b) / (HC p,T)) * (s *' p))))) + (- (HM f,T)) by POLYNOM1:def 23
.= (rf + (- (((rf . b) / (HC p,T)) * (s *' p)))) + ((HM f,T) + (- (HM f,T))) by POLYNOM1:80
.= (rf - (((rf . b) / (HC p,T)) * (s *' p))) + ((HM f,T) + (- (HM f,T))) by POLYNOM1:def 23
.= (rf - (((rf . b) / (HC p,T)) * (s *' p))) + ((HM f,T) - (HM f,T)) by POLYNOM1:def 23
.= (rf - (((rf . b) / (HC p,T)) * (s *' p))) + (0_ n,L) by POLYNOM1:83
.= rf - (((rf . b) / (HC p,T)) * (s *' p)) by POLYNOM1:82 ;
then rf reduces_to Red g,T,p,b,T by A10, A22, A26, Def5;
then rf reduces_to Red g,T,p,T by Def6;
then [(Support (Red g,T)),(Support rf)] in FinOrd RelStr(# (Bags n),T #) by A7, A25, XCMPLX_1:2;
then Red g,T <= Red f,T,T by Def2;
then g <= f,T by A13, A17, Lm16;
hence [(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by Def2; :: 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;

A27: for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A6);
consider k being Nat such that
A28: card (Support f) = k ;
[(Support g),(Support f)] in FinOrd RelStr(# (Bags n),T #) by A1, A27, A28;
then g <= f,T by Def2;
hence g < f,T by A3, Def3; :: thesis: verum