let n be Ordinal; :: thesis:
let T be connected TermOrder of n; :: thesis:
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis:
let P be Subset of (Polynom-Ring n,L); :: thesis:
let f, g be Element of (Polynom-Ring n,L); :: thesis:
set R = PolyRedRel P,T;
set PR = Polynom-Ring n,L;
defpred S₁[ Nat] means for f, g being Element of (Polynom-Ring n,L) st (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,g holds
for p being RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) st p . 1 = f & p . (len p) = g & len p = $1 holds
f,g are_congruent_mod P -Ideal ;
assume f,g are_convertible_wrt PolyRedRel P,T ; :: thesis:
then A1: (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,g by REWRITE1:def 4;
then consider p being RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) such that
A2: ( p . 1 = f & p . (len p) = g ) by REWRITE1:def 3;
A3: 0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;

A4: now

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

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

let f, g be Element of (Polynom-Ring n,L); :: thesis:
assume (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,g ; :: thesis:
let p be RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ); :: thesis:
assume that
A7: p . 1 = f and
A8: p . (len p) = g and
A9: len p = k + 1 ; :: thesis:
A10: dom p = Seg (k + 1) by A9, FINSEQ_1:def 3;
then A11: k + 1 in dom p by FINSEQ_1:6;
set q = p | (Seg k);
reconsider q = p | (Seg k) as FinSequence by FINSEQ_1:19;
A12: k <= k + 1 by NAT_1:11;
then A13: dom q = Seg k by A9, FINSEQ_1:21;
then A14: k in dom q by A5, FINSEQ_1:3;
set h = q . (len q);
A15: len q = k by A9, A12, FINSEQ_1:21;
k in dom p by A5, A10, A12, FINSEQ_1:3;
then [(p . k),(p . (k + 1))] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) by A11, REWRITE1:def 2;
then [(q . (len q)),g] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) by A8, A9, A15, A14, FUNCT_1:70;
then A16: ( [(q . (len q)),g] in PolyRedRel P,T or [(q . (len q)),g] in (PolyRedRel P,T) ~ ) by XBOOLE_0:def 3;

A17: now

per cases in PolyRedRel P,T or [g,(q . (len q))] in PolyRedRel P,T ) by A16, RELAT_1:def 7;

case [(q . (len q)),g] in PolyRedRel P,T ; :: thesis:

then consider h9, g9 being set such that
A18: [(q . (len q)),g] = [h9,g9] and
A19: h9 in NonZero (Polynom-Ring n,L) and
g9 in the carrier of (Polynom-Ring n,L) by RELSET_1:6;
q . (len q) = [h9,g9] `1 by A18, MCART_1:def 1
.= h9 by MCART_1:def 1 ;
hence ( q . (len q) in the carrier of (Polynom-Ring n,L) \ {(0_ n,L)} & q . (len q) in the carrier of (Polynom-Ring n,L) & g in the carrier of (Polynom-Ring n,L) ) by A19, POLYNOM1:def 27; :: thesis:

end;

case [g,(q . (len q))] in PolyRedRel P,T ; :: thesis:

then consider h9, g9 being set such that
A20: [g,(q . (len q))] = [h9,g9] and
A21: ( h9 in NonZero (Polynom-Ring n,L) & g9 in the carrier of (Polynom-Ring n,L) ) by RELSET_1:6;
A22: q . (len q) = [h9,g9] `2 by A20, MCART_1:def 2
.= g9 by MCART_1:def 2 ;
g = [h9,g9] `1 by A20, MCART_1:def 1
.= h9 by MCART_1:def 1 ;
hence ( g in the carrier of (Polynom-Ring n,L) \ {(0_ n,L)} & g in the carrier of (Polynom-Ring n,L) & q . (len q) in the carrier of (Polynom-Ring n,L) ) by A21, A22, POLYNOM1:def 27; :: thesis:

end;

end;

end;

let i be Element of NAT ; :: thesis:
assume that
A23: i in dom q and
A24: i + 1 in dom q ; :: thesis:
i + 1 <= k by A13, A24, FINSEQ_1:3;
then A25: i + 1 <= k + 1 by A12, XXREAL_0:2;
i <= k by A13, A23, FINSEQ_1:3;
then A26: i <= k + 1 by A12, XXREAL_0:2;
1 <= i + 1 by A13, A24, FINSEQ_1:3;
then A27: i + 1 in dom p by A10, A25, FINSEQ_1:3;
1 <= i by A13, A23, FINSEQ_1:3;
then i in dom p by A10, A26, FINSEQ_1:3;
then A28: [(p . i),(p . (i + 1))] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) by A27, REWRITE1:def 2;
p . i = q . i by A23, FUNCT_1:70;
hence [(q . i),(q . (i + 1))] in (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) by A24, A28, FUNCT_1:70; :: thesis:

end;

then reconsider q = q as RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) by A5, A15, REWRITE1:def 2;
reconsider h = q . (len q) as Polynomial of n,L by A17, POLYNOM1:def 27;
reconsider h9 = h as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider h9 = h9 as Element of (Polynom-Ring n,L) ;
1 in dom q by A5, A13, FINSEQ_1:3;
then A29: q . 1 = f by A7, FUNCT_1:70;
then (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,h by REWRITE1:def 3;
then A30: f,h9 are_congruent_mod P -Ideal by A6, A9, A12, A29, FINSEQ_1:21;

per cases in PolyRedRel P,T or [g,h] in PolyRedRel P,T ) by A16, RELAT_1:def 7;

case A31: [h,g] in PolyRedRel P,T ; :: thesis:

then consider h9, g9 being set such that
A32: [h,g] = [h9,g9] and
A33: h9 in NonZero (Polynom-Ring n,L) and
A34: g9 in the carrier of (Polynom-Ring n,L) by RELSET_1:6;
A35: h = [h9,g9] `1 by A32, MCART_1:def 1
.= h9 by MCART_1:def 1 ;
not h9 in {(0_ n,L)} by A3, A33, XBOOLE_0:def 5;
then h9 <> 0_ n,L by TARSKI:def 1;
then reconsider h = h as non-zero Polynomial of n,L by A35, POLYNOM7:def 2;
A36: g = [h9,g9] `2 by A32, MCART_1:def 2
.= g9 by MCART_1:def 2 ;
reconsider g9 = g9 as Polynomial of n,L by A34, POLYNOM1:def 27;
reconsider h9 = h as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider h9 = h9 as Element of (Polynom-Ring n,L) ;
h reduces_to g9,P,T by A31, A36, Def13;
then h9,g are_congruent_mod P -Ideal by A36, Lm19;
then f,g are_congruent_mod P -Ideal by A30, Th54;
hence f - g in P -Ideal by Def14; :: thesis:

end;

case A37: [g,h] in PolyRedRel P,T ; :: thesis:

then consider g9, h9 being set such that
A38: [g,h] = [g9,h9] and
A39: g9 in NonZero (Polynom-Ring n,L) and
A40: h9 in the carrier of (Polynom-Ring n,L) by RELSET_1:6;
A41: g = [g9,h9] `1 by A38, MCART_1:def 1
.= g9 by MCART_1:def 1 ;
not g9 in {(0_ n,L)} by A3, A39, XBOOLE_0:def 5;
then A42: g9 <> 0_ n,L by TARSKI:def 1;
A43: h = [g9,h9] `2 by A38, MCART_1:def 2
.= h9 by MCART_1:def 2 ;
then reconsider h = h as Element of (Polynom-Ring n,L) by A40;
reconsider h9 = h9 as Polynomial of n,L by A43;
reconsider g9 = g as non-zero Polynomial of n,L by A41, A42, POLYNOM1:def 27, POLYNOM7:def 2;
reconsider gg = g9 as Element of (Polynom-Ring n,L) ;
reconsider gg = gg as Element of (Polynom-Ring n,L) ;
reconsider h = h as Element of (Polynom-Ring n,L) ;
g9 reduces_to h9,P,T by A37, A43, Def13;
then h,gg are_congruent_mod P -Ideal by A43, Lm19, Th53;
then f,gg are_congruent_mod P -Ideal by A30, Th54;
hence f - g in P -Ideal by Def14; :: thesis:

end;

end;

end;

hence f,g are_congruent_mod P -Ideal by Def14; :: thesis:

end;

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

end;

end;

let f, g be Element of (Polynom-Ring n,L); :: thesis:
assume (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ) reduces f,g ; :: thesis:
let p be RedSequence of (PolyRedRel P,T) \/ ((PolyRedRel P,T) ~ ); :: thesis:
assume ( p . 1 = f & p . (len p) = g & len p = 1 ) ; :: thesis:
then A45: f - g = 0. (Polynom-Ring n,L) by RLVECT_1:28;
0. (Polynom-Ring n,L) in P -Ideal by IDEAL_1:3;
hence f,g are_congruent_mod P -Ideal by A45, Def14; :: thesis:

end;

A46: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A44, A4);
consider k being Nat such that
A47: len p = k ;
1 <= k by A47, NAT_1:14;
hence f,g are_congruent_mod P -Ideal by A46, A1, A2, A47; :: thesis: