let n be Nat; :: 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 P be non empty Subset of (Polynom-Ring (n,L)); :: thesis:
let f, g be Element of (Polynom-Ring (n,L)); :: thesis:
set PR = Polynom-Ring (n,L);
defpred S₁[ Nat] means for f, g being Element of (Polynom-Ring (n,L))
for p being LeftLinearCombination of P st Sum p = g - f & len p = $1 holds
f,g are_convertible_wrt PolyRedRel (P,T);

let k be Nat; :: thesis:
assume A1: S₁[k] ; :: thesis:

let f, g be Element of (Polynom-Ring (n,L)); :: thesis:
let p be LeftLinearCombination of P; :: thesis:
assume that
A2: Sum p = g - f and
A3: len p = k + 1 ; :: thesis:

set h = f + (p /. (k + 1));
set q = p | (Seg k);
reconsider q = p | (Seg k) as FinSequence by FINSEQ_1:15;
dom p = Seg (k + 1) by A3, FINSEQ_1:def 3;
then consider u being Element of (Polynom-Ring (n,L)), a being Element of P such that
A4: p /. (k + 1) = u * a by FINSEQ_1:4, IDEAL_1:def 9;
reconsider u9 = u, a9 = a as Element of (Polynom-Ring (n,L)) ;
reconsider u9 = u9, a9 = a9 as Polynomial of n,L by POLYNOM1:def 11;
A5: p /. (k + 1) = u9 *' a9 by A4, POLYNOM1:def 11;
k <= k + 1 by NAT_1:11;
then A6: len q = k by A3, FINSEQ_1:17;
reconsider q = q as LeftLinearCombination of P by IDEAL_1:42;
A7: Sum p = (Sum q) + (p /. (k + 1)) by A3, Lm6;
then (Sum p) - (p /. (k + 1)) = ((Sum q) + (p /. (k + 1))) + (- (p /. (k + 1)))
.= (Sum q) + ((p /. (k + 1)) + (- (p /. (k + 1)))) by RLVECT_1:def 3
.= (Sum q) + (0. (Polynom-Ring (n,L))) by RLVECT_1:5
.= Sum q by RLVECT_1:4 ;
then Sum q = (g - f) + (- (p /. (k + 1))) by A2
.= (g + (- f)) + (- (p /. (k + 1)))
.= g + ((- f) + (- (p /. (k + 1)))) by RLVECT_1:def 3
.= g + (- (f + (p /. (k + 1)))) by RLVECT_1:31
.= g - (f + (p /. (k + 1))) ;
then A8: f + (p /. (k + 1)),g are_convertible_wrt PolyRedRel (P,T) by A1, A6;

case ( a <> 0_ (n,L) & u <> 0_ (n,L) ) ; :: thesis:

then f,f + (p /. (k + 1)) are_convertible_wrt PolyRedRel (P,T) by A4, Lm20;
hence f,g are_convertible_wrt PolyRedRel (P,T) by A8, REWRITE1:30; :: thesis:

end;

case A9: ( a = 0_ (n,L) or u = 0_ (n,L) ) ; :: thesis:

reconsider sumq = Sum q as Polynomial of n,L by POLYNOM1:def 11;

per cases by A9;

case a = 0_ (n,L) ; :: thesis:

hence p /. (k + 1) = 0_ (n,L) by A5, POLYNOM1:28; :: thesis:

end;

case u = 0_ (n,L) ; :: thesis:

hence p /. (k + 1) = 0_ (n,L) by A5, Th5; :: thesis:

end;

end;

end;

then Sum p = sumq + (0_ (n,L)) by A7, POLYNOM1:def 11
.= Sum q by POLYNOM1:23 ;
hence f,g are_convertible_wrt PolyRedRel (P,T) by A1, A2, A6; :: thesis:

end;

end;

end;

hence f,g are_convertible_wrt PolyRedRel (P,T) ; :: thesis:

end;

hence f,g are_convertible_wrt PolyRedRel (P,T) ; :: thesis:

end;

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

end;

then A10: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A11: S₁[ 0 ]

let f, g be Element of (Polynom-Ring (n,L)); :: thesis:
let p be LeftLinearCombination of P; :: thesis:
assume that
A12: Sum p = g - f and
A13: len p = 0 ; :: thesis:
p = <*> the carrier of (Polynom-Ring (n,L)) by A13;
then Sum p = 0. (Polynom-Ring (n,L)) by RLVECT_1:43;
then f = g by A12, RLVECT_1:21;
hence f,g are_convertible_wrt PolyRedRel (P,T) by REWRITE1:26; :: thesis:

end;

A14: for k being Nat holds S₁[k] from NAT_1:sch 2(A11, A10);
assume f,g are_congruent_mod P -Ideal ; :: thesis:
then g,f are_congruent_mod P -Ideal by Th53;
then g - f in P -Ideal ;
then g - f in P -LeftIdeal by IDEAL_1:63;
then consider p being LeftLinearCombination of P such that
A15: Sum p = g - f by IDEAL_1:61;
ex k being Nat st len p = k ;
hence f,g are_convertible_wrt PolyRedRel (P,T) by A14, A15; :: thesis: