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

A4: now :: thesis: for k being Nat st 1 <= k & S₁[k] holds
S₁[k + 1]

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

proof

let f, g, h be Polynomial of n,L; :: thesis: ( f - g = h implies for h1 being Polynomial of n,L
for p being RedSequence of PolyRedRel (P,T) st p . 1 = h & p . (len p) = h1 & len p = k + 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 ) )
assume A7: f - g = h ; :: thesis: for h1 being Polynomial of n,L
for p being RedSequence of PolyRedRel (P,T) st p . 1 = h & p . (len p) = h1 & len p = k + 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 )
let h1 be Polynomial of n,L; :: thesis: for p being RedSequence of PolyRedRel (P,T) st p . 1 = h & p . (len p) = h1 & len p = k + 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 )
let r be RedSequence of PolyRedRel (P,T); :: thesis: ( r . 1 = h & r . (len r) = h1 & len r = k + 1 implies ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 ) )
assume that
A8: r . 1 = h and
A9: r . (len r) = h1 and
A10: len r = k + 1 ; :: thesis: ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 )
set h2 = r . k;
A11: dom r = Seg (k + 1) by A10, FINSEQ_1:def 3;
1 <= k + 1 by NAT_1:11;
then A12: k + 1 in dom r by A11, FINSEQ_1:1;
k <= k + 1 by NAT_1:11;
then k in dom r by A5, A11, FINSEQ_1:1;
then A13: [(r . k),(r . (k + 1))] in PolyRedRel (P,T) by A12, REWRITE1:def 2;
then consider x, y being object such that
A14: x in NonZero (Polynom-Ring (n,L)) and
y in the carrier of (Polynom-Ring (n,L)) and
A15: [(r . k),(r . (k + 1))] = [x,y] by ZFMISC_1:def 2;
A16: r . k = x by A15, XTUPLE_0:1;
then reconsider h2 = r . k as Polynomial of n,L by A14, POLYNOM1:def 11;
0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;
then not r . k in {(0_ (n,L))} by A14, A16, XBOOLE_0:def 5;
then r . k <> 0_ (n,L) by TARSKI:def 1;
then reconsider h2 = h2 as non-zero Polynomial of n,L by POLYNOM7:def 1;
h2 reduces_to h1,P,T by A9, A10, A13, Def13;
then consider p being Polynomial of n,L such that
A17: p in P and
A18: h2 reduces_to h1,p,T ;
consider b being bag of n such that
A19: h2 reduces_to h1,p,b,T by A18;
set q = r | (Seg k);
reconsider q = r | (Seg k) as FinSequence by FINSEQ_1:15;
A20: k <= k + 1 by NAT_1:11;
then A21: dom q = Seg k by A10, FINSEQ_1:17;
A22: dom r = Seg (k + 1) by A10, FINSEQ_1:def 3;

A23: now :: thesis: for i being Nat st i in dom q & i + 1 in dom q holds
[(q . i),(q . (i + 1))] in PolyRedRel (P,T)

let i be Nat; :: thesis: ( i in dom q & i + 1 in dom q implies [(q . i),(q . (i + 1))] in PolyRedRel (P,T) )
assume that
A24: i in dom q and
A25: i + 1 in dom q ; :: thesis: [(q . i),(q . (i + 1))] in PolyRedRel (P,T)
i + 1 <= k by A21, A25, FINSEQ_1:1;
then A26: i + 1 <= k + 1 by A20, XXREAL_0:2;
i <= k by A21, A24, FINSEQ_1:1;
then A27: i <= k + 1 by A20, XXREAL_0:2;
1 <= i + 1 by A21, A25, FINSEQ_1:1;
then A28: i + 1 in dom r by A22, A26, FINSEQ_1:1;
1 <= i by A21, A24, FINSEQ_1:1;
then i in dom r by A22, A27, FINSEQ_1:1;
then A29: [(r . i),(r . (i + 1))] in PolyRedRel (P,T) by A28, REWRITE1:def 2;
r . i = q . i by A24, FUNCT_1:47;
hence [(q . i),(q . (i + 1))] in PolyRedRel (P,T) by A25, A29, FUNCT_1:47; :: thesis: verum

end;

len q = k by A10, A20, FINSEQ_1:17;
then reconsider q = q as RedSequence of PolyRedRel (P,T) by A5, A23, REWRITE1:def 2;
A30: k in dom q by A5, A21, FINSEQ_1:1;
1 in dom q by A5, A21, FINSEQ_1:1;
then A31: q . 1 = h by A8, FUNCT_1:47;
q . (len q) = q . k by A10, A20, FINSEQ_1:17
.= h2 by A30, FUNCT_1:47 ;
then consider f2, g2 being Polynomial of n,L such that
A32: f2 - g2 = h2 and
A33: PolyRedRel (P,T) reduces f,f2 and
A34: PolyRedRel (P,T) reduces g,g2 by A6, A7, A10, A20, A31, FINSEQ_1:17;
consider s being bag of n such that
A35: s + (HT (p,T)) = b and
A36: h1 = h2 - (((h2 . b) / (HC (p,T))) * (s *' p)) by A19;
set f1 = f2 - (((f2 . b) / (HC (p,T))) * (s *' p));
set g1 = g2 - (((g2 . b) / (HC (p,T))) * (s *' p));
A37: ((f2 . b) / (HC (p,T))) + (- ((g2 . b) / (HC (p,T)))) = ((f2 . b) * ((HC (p,T)) ")) + (- ((g2 . b) / (HC (p,T))))
.= ((f2 . b) * ((HC (p,T)) ")) + (- ((g2 . b) * ((HC (p,T)) ")))
.= ((f2 . b) * ((HC (p,T)) ")) + ((- (g2 . b)) * ((HC (p,T)) ")) by VECTSP_1:9
.= ((f2 . b) + (- (g2 . b))) * ((HC (p,T)) ") by VECTSP_1:def 7
.= ((f2 . b) + ((- g2) . b)) * ((HC (p,T)) ") by POLYNOM1:17
.= ((f2 + (- g2)) . b) * ((HC (p,T)) ") by POLYNOM1:15
.= ((f2 - g2) . b) * ((HC (p,T)) ") by POLYNOM1:def 7
.= ((f2 - g2) . b) / (HC (p,T)) ;

A38: now :: thesis: ( ( not b in Support g2 & PolyRedRel (P,T) reduces g,g2 - (((g2 . b) / (HC (p,T))) * (s *' p)) ) or ( b in Support g2 & PolyRedRel (P,T) reduces g,g2 - (((g2 . b) / (HC (p,T))) * (s *' p)) ) )

per cases ( not b in Support g2 or b in Support g2 ) ;

case A39: not b in Support g2 ; :: thesis: PolyRedRel (P,T) reduces g,g2 - (((g2 . b) / (HC (p,T))) * (s *' p))

b is Element of Bags n by PRE_POLY:def 12;
then g2 . b = 0. L by A39, POLYNOM1:def 4;
then g2 - (((g2 . b) / (HC (p,T))) * (s *' p)) = g2 - (((0. L) * ((HC (p,T)) ")) * (s *' p))
.= g2 - ((0. L) * (s *' p))
.= g2 - (0_ (n,L)) by Th8
.= g2 by Th4 ;
hence PolyRedRel (P,T) reduces g,g2 - (((g2 . b) / (HC (p,T))) * (s *' p)) by A34; :: thesis: verum

end;

case A40: b in Support g2 ; :: thesis: PolyRedRel (P,T) reduces g,g2 - (((g2 . b) / (HC (p,T))) * (s *' p))

then g2 <> 0_ (n,L) by POLYNOM7:1;
then reconsider g2 = g2 as non-zero Polynomial of n,L by POLYNOM7:def 1;
( g2 <> 0_ (n,L) & p <> 0_ (n,L) ) by A18, Lm18, POLYNOM7:def 1;
then g2 reduces_to g2 - (((g2 . b) / (HC (p,T))) * (s *' p)),p,b,T by A35, A40;
then g2 reduces_to g2 - (((g2 . b) / (HC (p,T))) * (s *' p)),p,T ;
then g2 reduces_to g2 - (((g2 . b) / (HC (p,T))) * (s *' p)),P,T by A17;
then [g2,(g2 - (((g2 . b) / (HC (p,T))) * (s *' p)))] in PolyRedRel (P,T) by Def13;
then PolyRedRel (P,T) reduces g2,g2 - (((g2 . b) / (HC (p,T))) * (s *' p)) by REWRITE1:15;
hence PolyRedRel (P,T) reduces g,g2 - (((g2 . b) / (HC (p,T))) * (s *' p)) by A34, REWRITE1:16; :: thesis: verum

end;

end;

end;

A41: now :: thesis: ( ( not b in Support f2 & PolyRedRel (P,T) reduces f,f2 - (((f2 . b) / (HC (p,T))) * (s *' p)) ) or ( b in Support f2 & PolyRedRel (P,T) reduces f,f2 - (((f2 . b) / (HC (p,T))) * (s *' p)) ) )

per cases ( not b in Support f2 or b in Support f2 ) ;

case A42: not b in Support f2 ; :: thesis: PolyRedRel (P,T) reduces f,f2 - (((f2 . b) / (HC (p,T))) * (s *' p))

b is Element of Bags n by PRE_POLY:def 12;
then f2 . b = 0. L by A42, POLYNOM1:def 4;
then f2 - (((f2 . b) / (HC (p,T))) * (s *' p)) = f2 - (((0. L) * ((HC (p,T)) ")) * (s *' p))
.= f2 - ((0. L) * (s *' p))
.= f2 - (0_ (n,L)) by Th8
.= f2 by Th4 ;
hence PolyRedRel (P,T) reduces f,f2 - (((f2 . b) / (HC (p,T))) * (s *' p)) by A33; :: thesis: verum

end;

case A43: b in Support f2 ; :: thesis: PolyRedRel (P,T) reduces f,f2 - (((f2 . b) / (HC (p,T))) * (s *' p))

then f2 <> 0_ (n,L) by POLYNOM7:1;
then reconsider f2 = f2 as non-zero Polynomial of n,L by POLYNOM7:def 1;
( f2 <> 0_ (n,L) & p <> 0_ (n,L) ) by A18, Lm18, POLYNOM7:def 1;
then f2 reduces_to f2 - (((f2 . b) / (HC (p,T))) * (s *' p)),p,b,T by A35, A43;
then f2 reduces_to f2 - (((f2 . b) / (HC (p,T))) * (s *' p)),p,T ;
then f2 reduces_to f2 - (((f2 . b) / (HC (p,T))) * (s *' p)),P,T by A17;
then [f2,(f2 - (((f2 . b) / (HC (p,T))) * (s *' p)))] in PolyRedRel (P,T) by Def13;
then PolyRedRel (P,T) reduces f2,f2 - (((f2 . b) / (HC (p,T))) * (s *' p)) by REWRITE1:15;
hence PolyRedRel (P,T) reduces f,f2 - (((f2 . b) / (HC (p,T))) * (s *' p)) by A33, REWRITE1:16; :: thesis: verum

end;

end;

end;

A44: - (- (((g2 . b) / (HC (p,T))) * (s *' p))) = ((g2 . b) / (HC (p,T))) * (s *' p) by POLYNOM1:19;
A45: ((- ((f2 . b) / (HC (p,T)))) * (s *' p)) + (((g2 . b) / (HC (p,T))) * (s *' p)) = ((- ((f2 . b) / (HC (p,T)))) + ((g2 . b) / (HC (p,T)))) * (s *' p) by Th10
.= - (- (((- ((f2 . b) / (HC (p,T)))) + ((g2 . b) / (HC (p,T)))) * (s *' p))) by POLYNOM1:19 ;
(f2 - (((f2 . b) / (HC (p,T))) * (s *' p))) - (g2 - (((g2 . b) / (HC (p,T))) * (s *' p))) = (f2 - (((f2 . b) / (HC (p,T))) * (s *' p))) + (- (g2 - (((g2 . b) / (HC (p,T))) * (s *' p)))) by POLYNOM1:def 7
.= (f2 + (- (((f2 . b) / (HC (p,T))) * (s *' p)))) + (- (g2 - (((g2 . b) / (HC (p,T))) * (s *' p)))) by POLYNOM1:def 7
.= (f2 + (- (((f2 . b) / (HC (p,T))) * (s *' p)))) + (- (g2 + (- (((g2 . b) / (HC (p,T))) * (s *' p))))) by POLYNOM1:def 7
.= (f2 + (- (((f2 . b) / (HC (p,T))) * (s *' p)))) + ((- g2) + (- (- (((g2 . b) / (HC (p,T))) * (s *' p))))) by Th1
.= ((f2 + (- (((f2 . b) / (HC (p,T))) * (s *' p)))) + (- g2)) + (((g2 . b) / (HC (p,T))) * (s *' p)) by A44, POLYNOM1:21
.= ((- (((f2 . b) / (HC (p,T))) * (s *' p))) + (f2 + (- g2))) + (((g2 . b) / (HC (p,T))) * (s *' p)) by POLYNOM1:21
.= (f2 + (- g2)) + ((- (((f2 . b) / (HC (p,T))) * (s *' p))) + (((g2 . b) / (HC (p,T))) * (s *' p))) by POLYNOM1:21
.= (f2 - g2) + ((- (((f2 . b) / (HC (p,T))) * (s *' p))) + (((g2 . b) / (HC (p,T))) * (s *' p))) by POLYNOM1:def 7
.= (f2 - g2) + (((- ((f2 . b) / (HC (p,T)))) * (s *' p)) + (((g2 . b) / (HC (p,T))) * (s *' p))) by Th9
.= (f2 - g2) + (- ((- ((- ((f2 . b) / (HC (p,T)))) + ((g2 . b) / (HC (p,T))))) * (s *' p))) by A45, Th9
.= (f2 - g2) - ((- ((- ((f2 . b) / (HC (p,T)))) + ((g2 . b) / (HC (p,T))))) * (s *' p)) by POLYNOM1:def 7
.= (f2 - g2) - (((- (- ((f2 . b) / (HC (p,T))))) + (- ((g2 . b) / (HC (p,T))))) * (s *' p)) by RLVECT_1:31
.= h1 by A32, A36, A37, RLVECT_1:17 ;
hence ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 ) by A41, A38; :: thesis: verum

end;

end;

A46: S₁[1]

proof

let f, g, h be Polynomial of n,L; :: thesis: ( f - g = h implies for h1 being Polynomial of n,L
for p being RedSequence of PolyRedRel (P,T) st p . 1 = h & p . (len p) = h1 & len p = 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 ) )
assume A47: f - g = h ; :: thesis: for h1 being Polynomial of n,L
for p being RedSequence of PolyRedRel (P,T) st p . 1 = h & p . (len p) = h1 & len p = 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 )
let h1 be Polynomial of n,L; :: thesis: for p being RedSequence of PolyRedRel (P,T) st p . 1 = h & p . (len p) = h1 & len p = 1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 )
let p be RedSequence of PolyRedRel (P,T); :: thesis: ( p . 1 = h & p . (len p) = h1 & len p = 1 implies ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 ) )
assume A48: ( p . 1 = h & p . (len p) = h1 & len p = 1 ) ; :: thesis: ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 )
take f ; :: thesis: ex g1 being Polynomial of n,L st
( f - g1 = h1 & PolyRedRel (P,T) reduces f,f & PolyRedRel (P,T) reduces g,g1 )
take g ; :: thesis: ( f - g = h1 & PolyRedRel (P,T) reduces f,f & PolyRedRel (P,T) reduces g,g )
thus ( f - g = h1 & PolyRedRel (P,T) reduces f,f & PolyRedRel (P,T) reduces g,g ) by A47, A48, REWRITE1:12; :: thesis: verum

end;

A49: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A46, A4);
consider k being Nat such that
A50: len p = k ;
1 <= k by A50, NAT_1:14;
hence ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 ) by A1, A49, A3, A50; :: thesis: verum