let n be Nat; :: 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 P being non empty Subset of (Polynom-Ring n,L)
for f, g being Element of (Polynom-Ring n,L) st f,g are_congruent_mod P -Ideal holds
f,g are_convertible_wrt PolyRedRel P,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 P being non empty Subset of (Polynom-Ring n,L)
for f, g being Element of (Polynom-Ring n,L) st f,g are_congruent_mod P -Ideal holds
f,g are_convertible_wrt PolyRedRel P,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 P being non empty Subset of (Polynom-Ring n,L)
for f, g being Element of (Polynom-Ring n,L) st f,g are_congruent_mod P -Ideal holds
f,g are_convertible_wrt PolyRedRel P,T
let P be non empty Subset of (Polynom-Ring n,L); :: thesis: for f, g being Element of (Polynom-Ring n,L) st f,g are_congruent_mod P -Ideal holds
f,g are_convertible_wrt PolyRedRel P,T
let f, g be Element of (Polynom-Ring n,L); :: thesis: ( f,g are_congruent_mod P -Ideal implies f,g are_convertible_wrt PolyRedRel P,T )
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;

now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A1: S₁[k] ; :: thesis: S₁[k + 1]

now

let f, g be Element of (Polynom-Ring n,L); :: thesis: for p being LeftLinearCombination of P st Sum p = g - f & len p = k + 1 holds
f,g are_convertible_wrt PolyRedRel P,T
let p be LeftLinearCombination of P; :: thesis: ( Sum p = g - f & len p = k + 1 implies f,g are_convertible_wrt PolyRedRel P,T )
assume that
A2: Sum p = g - f and
A3: len p = k + 1 ; :: thesis: f,g are_convertible_wrt PolyRedRel P,T

now

set h = f + (p /. (k + 1));
set q = p | (Seg k);
reconsider q = p | (Seg k) as FinSequence by FINSEQ_1:19;
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:6, IDEAL_1:def 10;
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 27;
A5: p /. (k + 1) = u9 *' a9 by A4, POLYNOM1:def 27;
k <= k + 1 by NAT_1:11;
then A6: len q = k by A3, FINSEQ_1:21;
k in NAT by ORDINAL1:def 13;
then 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))) by RLVECT_1:def 14
.= (Sum q) + ((p /. (k + 1)) + (- (p /. (k + 1)))) by RLVECT_1:def 6
.= (Sum q) + (0. (Polynom-Ring n,L)) by RLVECT_1:16
.= Sum q by RLVECT_1:10 ;
then Sum q = (g - f) + (- (p /. (k + 1))) by A2, RLVECT_1:def 14
.= (g + (- f)) + (- (p /. (k + 1))) by RLVECT_1:def 14
.= g + ((- f) + (- (p /. (k + 1)))) by RLVECT_1:def 6
.= g + (- (f + (p /. (k + 1)))) by RLVECT_1:45
.= g - (f + (p /. (k + 1))) by RLVECT_1:def 14 ;
then A8: f + (p /. (k + 1)),g are_convertible_wrt PolyRedRel P,T by A1, A6;

now

per cases ( ( a <> 0_ n,L & u <> 0_ n,L ) or a = 0_ n,L or u = 0_ n,L ) ;

case ( a <> 0_ n,L & u <> 0_ n,L ) ; :: thesis: f,g are_convertible_wrt PolyRedRel P,T

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:31; :: thesis: verum

end;

case A9: ( a = 0_ n,L or u = 0_ n,L ) ; :: thesis: f,g are_convertible_wrt PolyRedRel P,T

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

now

per cases ( a = 0_ n,L or u = 0_ n,L ) by A9;

case a = 0_ n,L ; :: thesis: p /. (k + 1) = 0_ n,L

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

end;

case u = 0_ n,L ; :: thesis: p /. (k + 1) = 0_ n,L

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

end;

end;

end;

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

end;

end;

end;

hence f,g are_convertible_wrt PolyRedRel P,T ; :: thesis: verum

end;

hence f,g are_convertible_wrt PolyRedRel P,T ; :: thesis: verum

end;

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

end;

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

proof

let f, g be Element of (Polynom-Ring n,L); :: thesis: for p being LeftLinearCombination of P st Sum p = g - f & len p = 0 holds
f,g are_convertible_wrt PolyRedRel P,T
let p be LeftLinearCombination of P; :: thesis: ( Sum p = g - f & len p = 0 implies f,g are_convertible_wrt PolyRedRel P,T )
assume that
A12: Sum p = g - f and
A13: len p = 0 ; :: thesis: f,g are_convertible_wrt PolyRedRel P,T
p = <*> the carrier of (Polynom-Ring n,L) by A13;
then Sum p = 0. (Polynom-Ring n,L) by RLVECT_1:60;
then f = g by A12, RLVECT_1:35;
hence f,g are_convertible_wrt PolyRedRel P,T by REWRITE1:27; :: thesis: verum

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: f,g are_convertible_wrt PolyRedRel P,T
then g,f are_congruent_mod P -Ideal by Th53;
then g - f in P -Ideal by Def14;
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: verum