let n be Ordinal; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis:
let f, g be Polynomial of n,L; :: thesis:
let P be Subset of (Polynom-Ring (n,L)); :: thesis:
set R = PolyRedRel (P,T);
defpred S₁[ Nat] means for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
for p being RedSequence of PolyRedRel (P,T) st p . 1 = f & p . (len p) = g & len p = $1 holds
g <= f,T;
assume A1: PolyRedRel (P,T) reduces f,g ; :: thesis:
then consider p being RedSequence of PolyRedRel (P,T) such that
A2: ( p . 1 = f & p . (len p) = g ) by REWRITE1:def 3;

A3: now :: thesis:

let k be Nat; :: thesis:
assume A4: 1 <= k ; :: thesis:
thus ( S₁[k] implies S₁[k + 1] ) :: thesis:

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

let f, g be Polynomial of n,L; :: thesis:
assume PolyRedRel (P,T) reduces f,g ; :: thesis:
let p be RedSequence of PolyRedRel (P,T); :: thesis:
assume that
A6: p . 1 = f and
A7: p . (len p) = g and
A8: len p = k + 1 ; :: thesis:
A9: dom p = Seg (k + 1) by A8, FINSEQ_1:def 3;
then A10: k + 1 in dom p by FINSEQ_1:4;
set q = p | (Seg k);
reconsider q = p | (Seg k) as FinSequence by FINSEQ_1:15;
A11: k <= k + 1 by NAT_1:11;
then A12: dom q = Seg k by A8, FINSEQ_1:17;
then A13: k in dom q by A4, FINSEQ_1:1;
set h = q . (len q);
A14: len q = k by A8, A11, FINSEQ_1:17;
k in dom p by A4, A9, A11, FINSEQ_1:1;
then [(p . k),(p . (k + 1))] in PolyRedRel (P,T) by A10, REWRITE1:def 2;
then A15: [(q . (len q)),g] in PolyRedRel (P,T) by A7, A8, A14, A13, FUNCT_1:47;
then consider h9, g9 being object such that
A16: [(q . (len q)),g] = [h9,g9] and
A17: h9 in NonZero (Polynom-Ring (n,L)) and
g9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
A18: q . (len q) = h9 by A16, XTUPLE_0:1;

A19: now :: thesis:

let i be Nat; :: thesis:
assume that
A20: i in dom q and
A21: i + 1 in dom q ; :: thesis:
i + 1 <= k by A12, A21, FINSEQ_1:1;
then A22: i + 1 <= k + 1 by A11, XXREAL_0:2;
i <= k by A12, A20, FINSEQ_1:1;
then A23: i <= k + 1 by A11, XXREAL_0:2;
1 <= i + 1 by A12, A21, FINSEQ_1:1;
then A24: i + 1 in dom p by A9, A22, FINSEQ_1:1;
1 <= i by A12, A20, FINSEQ_1:1;
then i in dom p by A9, A23, FINSEQ_1:1;
then A25: [(p . i),(p . (i + 1))] in PolyRedRel (P,T) by A24, REWRITE1:def 2;
p . i = q . i by A20, FUNCT_1:47;
hence [(q . i),(q . (i + 1))] in PolyRedRel (P,T) by A21, A25, FUNCT_1:47; :: thesis:

end;

0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;
then not h9 in {(0_ (n,L))} by A17, XBOOLE_0:def 5;
then h9 <> 0_ (n,L) by TARSKI:def 1;
then reconsider h = q . (len q) as non-zero Polynomial of n,L by A17, A18, POLYNOM1:def 11, POLYNOM7:def 1;
reconsider q = q as RedSequence of PolyRedRel (P,T) by A4, A14, A19, REWRITE1:def 2;
1 in dom q by A4, A12, FINSEQ_1:1;
then A26: q . 1 = f by A6, FUNCT_1:47;
then PolyRedRel (P,T) reduces f,h by REWRITE1:def 3;
then A27: h <= f,T by A5, A8, A11, A26, FINSEQ_1:17;
h reduces_to g,P,T by A15, Def13;
then A28: ex r being Polynomial of n,L st
( r in P & h reduces_to g,r,T ) ;
reconsider h = h as non-zero Polynomial of n,L ;
g < h,T by A28, Th43;
then g <= h,T ;
hence g <= f,T by A27, Th27; :: thesis:

end;

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

end;

end;

A29: S₁[1] by Th25;
A30: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A29, A3);
consider k being Nat such that
A31: len p = k ;
1 <= k by A31, NAT_1:14;
hence A32: g <= f,T by A1, A30, A2, A31; :: thesis:

assume g <> 0_ (n,L) ; :: thesis:
then Support g <> {} by POLYNOM7:1;
then A33: HT (g,T) in Support g by TERMORD:def 6;
assume A34: not HT (g,T) <= HT (f,T),T ; :: thesis:

case HT (f,T) = HT (g,T) ; :: thesis:

hence contradiction by A34, TERMORD:6; :: thesis:

end;

case A35: HT (f,T) <> HT (g,T) ; :: thesis:

HT (g,T) <= HT (g,T),T by TERMORD:6;
then [(HT (g,T)),(HT (g,T))] in T by TERMORD:def 2;
then A36: 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 ( T is_connected_in field T & HT (f,T) in field T ) by RELAT_1:15, RELAT_2:def 14;
then ( [(HT (f,T)),(HT (g,T))] in T or [(HT (g,T)),(HT (f,T))] in T ) by A35, A36, RELAT_2:def 6;
then HT (f,T) <= HT (g,T),T by A34, TERMORD:def 2;
then A37: HT (f,T) < HT (g,T),T by A35, TERMORD:def 3;
then f < g,T by Lm15;
then f <= g,T ;
then Support f = Support g by A32, Th26;
then HT (g,T) <= HT (f,T),T by A33, TERMORD:def 6;
hence contradiction by A37, TERMORD:5; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

hence ( g = 0_ (n,L) or HT (g,T) <= HT (f,T),T ) ; :: thesis: