let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T
let p, q be Polynomial of n,L; :: thesis: ( Support q c= Support p implies q <= p,T )
assume A1: Support q c= Support p ; :: thesis: q <= p,T
defpred S₁[ Element of NAT ] means for f, g being Polynomial of n,L st Support f c= Support g & card (Support f) = $1 holds
f <= g,T;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]

now

set R = RelStr(# (Bags n),T #);
let f, g be Polynomial of n,L; :: thesis: ( Support f c= Support g & card (Support f) = k + 1 implies f <= g,T )
assume that
A4: Support f c= Support g and
A5: card (Support f) = k + 1 ; :: thesis: f <= g,T
set rf = Red f,T;
set rg = Red g,T;
A6: Support f <> {} by A5;
then A7: HT f,T in Support f by TERMORD:def 6;
f <> 0_ n,L by A6, POLYNOM7:1;
then A8: f is non-zero by POLYNOM7:def 2;
g <> 0_ n,L by A4, A7, POLYNOM7:1;
then A9: g is non-zero by POLYNOM7:def 2;

now

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

case A10: HT f,T = HT g,T ; :: thesis: f <= g,T

A11: Support (Red f,T) = (Support f) \ {(HT f,T)} by TERMORD:36;
A12: Support (Red g,T) = (Support g) \ {(HT g,T)} by TERMORD:36;

now

let u be set ; :: thesis: ( u in Support (Red f,T) implies u in Support (Red g,T) )
assume u in Support (Red f,T) ; :: thesis: u in Support (Red g,T)
then ( u in Support f & not u in {(HT f,T)} ) by A11, XBOOLE_0:def 5;
hence u in Support (Red g,T) by A4, A10, A12, XBOOLE_0:def 5; :: thesis: verum

end;

then A13: Support (Red f,T) c= Support (Red g,T) by TARSKI:def 3;
for u being set st u in {(HT f,T)} holds
u in Support f by A7, TARSKI:def 1;
then A14: {(HT f,T)} c= Support f by TARSKI:def 3;
A15: ( Support f,T <> {} & Support g,T <> {} ) by A4, A7, POLYRED:def 4;
A16: Support (Red f,T),T = Support (Red f,T) by POLYRED:def 4;
HT f,T in {(HT f,T)} by TARSKI:def 1;
then A17: not HT f,T in Support (Red f,T) by A11, XBOOLE_0:def 5;
A18: PosetMax (Support f,T) = HT g,T by A8, A10, POLYRED:24
.= PosetMax (Support g,T) by A9, POLYRED:24 ;
A19: Support (Red g,T),T = Support (Red g,T) by POLYRED:def 4;
A20: Support g,T = Support g by POLYRED:def 4;
then A21: (Support g,T) \ {(PosetMax (Support g,T))} = Support (Red g,T),T by A9, A12, A19, POLYRED:24;
(Support (Red f,T)) \/ {(HT f,T)} = (Support f) \/ {(HT f,T)} by A11, XBOOLE_1:39
.= Support f by A14, XBOOLE_1:12 ;
then (card (Support (Red f,T))) + 1 = k + 1 by A5, A17, CARD_2:54;
then Red f,T <= Red g,T,T by A3, A13;
then [(Support (Red f,T)),(Support (Red g,T))] in FinOrd RelStr(# (Bags n),T #) by POLYRED:def 2;
then A22: [(Support (Red f,T),T),(Support (Red g,T),T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A16, A19, BAGORDER:def 17;
A23: Support f,T = Support f by POLYRED:def 4;
then (Support f,T) \ {(PosetMax (Support f,T))} = Support (Red f,T),T by A8, A11, A16, POLYRED:24;
then [(Support f,T),(Support g,T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A22, A15, A18, A21, BAGORDER:36;
then [(Support f),(Support g)] in FinOrd RelStr(# (Bags n),T #) by A23, A20, BAGORDER:def 17;
hence f <= g,T by POLYRED:def 2; :: thesis: verum

end;

case A24: HT f,T <> HT g,T ; :: thesis: f <= g,T

now

assume HT g,T < HT f,T,T ; :: thesis: contradiction
then not HT f,T <= HT g,T,T by TERMORD:5;
hence contradiction by A4, A7, TERMORD:def 6; :: thesis: verum

end;

then HT f,T <= HT g,T,T by TERMORD:5;
then HT f,T < HT g,T,T by A24, TERMORD:def 3;
then f < g,T by POLYRED:32;
hence f <= g,T by POLYRED:def 3; :: thesis: verum

end;

end;

end;

hence f <= g,T ; :: thesis: verum

end;

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

end;

A25: ex k being Element of NAT st card (Support q) = k ;
A26: S₁[ 0 ]

proof

let f, g be Polynomial of n,L; :: thesis: ( Support f c= Support g & card (Support f) = 0 implies f <= g,T )
assume that
Support f c= Support g and
A27: card (Support f) = 0 ; :: thesis: f <= g,T
Support f = {} by A27;
then f = 0_ n,L by POLYNOM7:1;
hence f <= g,T by POLYRED:30; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A26, A2);
hence q <= p,T by A1, A25; :: thesis: verum