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 P be Subset of (Polynom-Ring (n,L)); :: thesis:
let f, g be Polynomial of n,L; :: thesis:
let m be Monomial of n,L; :: thesis:
assume A1: PolyRedRel (P,T) reduces f,g ; :: thesis:
set R = PolyRedRel (P,T);

per cases ;

suppose A2: m = 0_ (n,L) ; :: thesis:

then m *' f = 0_ (n,L) by Th5
.= m *' g by A2, Th5 ;
hence PolyRedRel (P,T) reduces m *' f,m *' g by REWRITE1:12; :: thesis:

end;

suppose m <> 0_ (n,L) ; :: thesis:

then reconsider m = m as non-zero Monomial of n,L by POLYNOM7:def 1;
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
PolyRedRel (P,T) reduces m *' f,m *' g;
consider p being RedSequence of PolyRedRel (P,T) such that
A3: ( p . 1 = f & p . (len p) = g ) by A1, REWRITE1:def 3;
consider k being Nat such that
A4: len p = k ;

A5: now :: thesis:

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

proof

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

now :: 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
A8: p . 1 = f and
A9: p . (len p) = g and
A10: len p = k + 1 ; :: thesis:
A11: dom p = Seg (k + 1) by A10, FINSEQ_1:def 3;
then A12: 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;
A13: k <= k + 1 by NAT_1:11;
then A14: dom q = Seg k by A10, FINSEQ_1:17;
then A15: k in dom q by A6, FINSEQ_1:1;
set h = q . (len q);
A16: len q = k by A10, A13, FINSEQ_1:17;
k in dom p by A6, A11, A13, FINSEQ_1:1;
then [(p . k),(p . (k + 1))] in PolyRedRel (P,T) by A12, REWRITE1:def 2;
then A17: [(q . (len q)),g] in PolyRedRel (P,T) by A9, A10, A16, A15, FUNCT_1:47;
then consider h9, g9 being object 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:2;
A20: q . (len q) = h9 by A18, XTUPLE_0:1;

A21: now :: thesis:

let i be Nat; :: thesis:
assume that
A22: i in dom q and
A23: i + 1 in dom q ; :: thesis:
i + 1 <= k by A14, A23, FINSEQ_1:1;
then A24: i + 1 <= k + 1 by A13, XXREAL_0:2;
i <= k by A14, A22, FINSEQ_1:1;
then A25: i <= k + 1 by A13, XXREAL_0:2;
1 <= i + 1 by A14, A23, FINSEQ_1:1;
then A26: i + 1 in dom p by A11, A24, FINSEQ_1:1;
1 <= i by A14, A22, FINSEQ_1:1;
then i in dom p by A11, A25, FINSEQ_1:1;
then A27: [(p . i),(p . (i + 1))] in PolyRedRel (P,T) by A26, REWRITE1:def 2;
p . i = q . i by A22, FUNCT_1:47;
hence [(q . i),(q . (i + 1))] in PolyRedRel (P,T) by A23, A27, 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 A19, 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 A19, A20, POLYNOM1:def 11, POLYNOM7:def 1;
h reduces_to g,P,T by A17, Def13;
then m *' h reduces_to m *' g,P,T by Th46;
then [(m *' h),(m *' g)] in PolyRedRel (P,T) by Def13;
then A28: PolyRedRel (P,T) reduces m *' h,m *' g by REWRITE1:15;
reconsider q = q as RedSequence of PolyRedRel (P,T) by A6, A16, A21, REWRITE1:def 2;
1 in dom q by A6, A14, FINSEQ_1:1;
then A29: q . 1 = f by A8, FUNCT_1:47;
then PolyRedRel (P,T) reduces f,h by REWRITE1:def 3;
then PolyRedRel (P,T) reduces m *' f,m *' h by A7, A10, A13, A29, FINSEQ_1:17;
hence PolyRedRel (P,T) reduces m *' f,m *' g by A28, REWRITE1:16; :: thesis:

end;

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

end;

end;

A30: S₁[1] by REWRITE1:12;
A31: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A30, A5);
1 <= k by A4, NAT_1:14;
hence PolyRedRel (P,T) reduces m *' f,m *' g by A1, A31, A3, A4; :: thesis:

end;

end;