let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, f1, g, p being Polynomial of n,L st PolyRedRel {p},T reduces f,f1 & ( for b1 being bag of 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, f1, g, p being Polynomial of n,L st PolyRedRel {p},T reduces f,f1 & ( for b1 being bag of 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for f, f1, g, p being Polynomial of n,L st PolyRedRel {p},T reduces f,f1 & ( for b1 being bag of 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 st b1 in Support g holds
not HT p,T divides b1 ) implies PolyRedRel {p},T reduces f + g,f1 + g )
assume A1: ( PolyRedRel {p},T reduces f,f1 & ( for b1 being bag of st b1 in Support g holds
not HT p,T divides b1 ) ) ; :: thesis: PolyRedRel {p},T reduces f + g,f1 + g
then consider R being RedSequence of PolyRedRel {p},T such that
A2: ( R . 1 = f & R . (len R) = f1 ) by REWRITE1:def 3;
defpred S₁[ Element of NAT ] means for q being Polynomial of n,L st q = R . $1 holds
PolyRedRel {p},T reduces f + g,q + g;
A3: S₁[1] by A2, REWRITE1:13;

A4: now

let k be Element of NAT ; :: thesis: ( 1 <= k & k < len R & S₁[k] implies S₁[k + 1] )
assume A5: ( 1 <= k & k < len R ) ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
1 < len R by A5, XXREAL_0:2;
then reconsider h = R . k as Polynomial of n,L by A5, Lm4;
A7: PolyRedRel {p},T reduces f + g,h + g by A6;

now

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
A9: k in dom R by A5, FINSEQ_3:27;
( 1 <= k + 1 & k + 1 <= len R ) by A5, NAT_1:13;
then k + 1 in dom R by FINSEQ_3:27;
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 A1, 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:16;
hence PolyRedRel {p},T reduces f + g,q + g by A7, REWRITE1:17; :: thesis: verum

end;

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

end;

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