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₁[ Nat] means for q being Polynomial of n,L st q = R . $1 holds
PolyRedRel ({p},T) reduces f + g,q + g;

A5: now :: thesis: for k being Element of NAT st 1 <= k & k < len R & S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis: ( 1 <= k & k < len R & S₁[k] implies S₁[k + 1] )
assume A6: ( 1 <= k & k < len R ) ; :: thesis: ( S₁[k] implies S₁[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₁[k] ; :: thesis: S₁[k + 1]
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

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;

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

end;

A10: 1 <= len R by NAT_1:14;
A11: S₁[1] by A3, REWRITE1:12;
for i being Element of NAT st 1 <= i & i <= len R holds
S₁[i] from INT_1:sch 7(A11, A5);
hence PolyRedRel ({p},T) reduces f + g,f1 + g by A4, A10; :: thesis: verum