let n be Ordinal; :: thesis: for T being connected admissible 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 f, f1, g, p being Polynomial of n,L st PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) holds

PolyRedRel ({p},T) reduces f + g,f1 + g

let T be connected admissible 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 f, f1, g, p being Polynomial of n,L st PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) holds

PolyRedRel ({p},T) reduces f + g,f1 + g

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, f1, g, p being Polynomial of n,L st PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) holds

PolyRedRel ({p},T) reduces f + g,f1 + g

let f, f1, g, p be Polynomial of n,L; :: thesis: ( PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) implies PolyRedRel ({p},T) reduces f + g,f1 + g )

assume that

A1: PolyRedRel ({p},T) reduces f,f1 and

A2: for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ; :: thesis: PolyRedRel ({p},T) reduces f + g,f1 + g

consider R being RedSequence of PolyRedRel ({p},T) such that

A3: R . 1 = f and

A4: R . (len R) = f1 by A1, REWRITE1:def 3;

defpred S_{1}[ Nat] means for q being Polynomial of n,L st q = R . $1 holds

PolyRedRel ({p},T) reduces f + g,q + g;

A11: S_{1}[1]
by A3, REWRITE1:12;

for i being Element of NAT st 1 <= i & i <= len R holds

S_{1}[i]
from INT_1:sch 7(A11, A5);

hence PolyRedRel ({p},T) reduces f + g,f1 + g by A4, A10; :: thesis: verum

for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f, f1, g, p being Polynomial of n,L st PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) holds

PolyRedRel ({p},T) reduces f + g,f1 + g

let T be connected admissible 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 f, f1, g, p being Polynomial of n,L st PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) holds

PolyRedRel ({p},T) reduces f + g,f1 + g

let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, f1, g, p being Polynomial of n,L st PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) holds

PolyRedRel ({p},T) reduces f + g,f1 + g

let f, f1, g, p be Polynomial of n,L; :: thesis: ( PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ) implies PolyRedRel ({p},T) reduces f + g,f1 + g )

assume that

A1: PolyRedRel ({p},T) reduces f,f1 and

A2: for b1 being bag of n st b1 in Support g holds

not HT (p,T) divides b1 ; :: thesis: PolyRedRel ({p},T) reduces f + g,f1 + g

consider R being RedSequence of PolyRedRel ({p},T) such that

A3: R . 1 = f and

A4: R . (len R) = f1 by A1, REWRITE1:def 3;

defpred S

PolyRedRel ({p},T) reduces f + g,q + g;

A5: now :: thesis: for k being Element of NAT st 1 <= k & k < len R & S_{1}[k] holds

S_{1}[k + 1]

A10:
1 <= len R
by NAT_1:14;S

let k be Element of NAT ; :: thesis: ( 1 <= k & k < len R & S_{1}[k] implies S_{1}[k + 1] )

assume A6: ( 1 <= k & k < len R ) ; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

then 1 < len R by XXREAL_0:2;

then reconsider h = R . k as Polynomial of n,L by A6, Lm4;

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then A7: PolyRedRel ({p},T) reduces f + g,h + g ;

_{1}[k + 1]
; :: thesis: verum

end;assume A6: ( 1 <= k & k < len R ) ; :: thesis: ( S

then 1 < len R by XXREAL_0:2;

then reconsider h = R . k as Polynomial of n,L by A6, Lm4;

assume S

then A7: PolyRedRel ({p},T) reduces f + g,h + g ;

now :: thesis: for q being Polynomial of n,L st q = R . (k + 1) holds

PolyRedRel ({p},T) reduces f + g,q + g

hence
SPolyRedRel ({p},T) reduces f + g,q + g

let q be Polynomial of n,L; :: thesis: ( q = R . (k + 1) implies PolyRedRel ({p},T) reduces f + g,q + g )

assume A8: q = R . (k + 1) ; :: thesis: PolyRedRel ({p},T) reduces f + g,q + g

( 1 <= k + 1 & k + 1 <= len R ) by A6, NAT_1:13;

then A9: k + 1 in dom R by FINSEQ_3:25;

k in dom R by A6, FINSEQ_3:25;

then [(R . k),(R . (k + 1))] in PolyRedRel ({p},T) by A9, REWRITE1:def 2;

then h reduces_to q,{p},T by A8, POLYRED:def 13;

then h + g reduces_to q + g,{p},T by A2, Th46;

then [(h + g),(q + g)] in PolyRedRel ({p},T) by POLYRED:def 13;

then PolyRedRel ({p},T) reduces h + g,q + g by REWRITE1:15;

hence PolyRedRel ({p},T) reduces f + g,q + g by A7, REWRITE1:16; :: thesis: verum

end;assume A8: q = R . (k + 1) ; :: thesis: PolyRedRel ({p},T) reduces f + g,q + g

( 1 <= k + 1 & k + 1 <= len R ) by A6, NAT_1:13;

then A9: k + 1 in dom R by FINSEQ_3:25;

k in dom R by A6, FINSEQ_3:25;

then [(R . k),(R . (k + 1))] in PolyRedRel ({p},T) by A9, REWRITE1:def 2;

then h reduces_to q,{p},T by A8, POLYRED:def 13;

then h + g reduces_to q + g,{p},T by A2, Th46;

then [(h + g),(q + g)] in PolyRedRel ({p},T) by POLYRED:def 13;

then PolyRedRel ({p},T) reduces h + g,q + g by REWRITE1:15;

hence PolyRedRel ({p},T) reduces f + g,q + g by A7, REWRITE1:16; :: thesis: verum

A11: S

for i being Element of NAT st 1 <= i & i <= len R holds

S

hence PolyRedRel ({p},T) reduces f + g,f1 + g by A4, A10; :: thesis: verum