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 P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces - f, - 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 P being Subset of (Polynom-Ring (n,L))
for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces - f, - g
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 being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces - f, - g
let P be Subset of (Polynom-Ring (n,L)); :: thesis: for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f,g holds
PolyRedRel (P,T) reduces - f, - g
let f, g be Polynomial of n,L; :: thesis: ( PolyRedRel (P,T) reduces f,g implies PolyRedRel (P,T) reduces - f, - g )
assume PolyRedRel (P,T) reduces f,g ; :: thesis: PolyRedRel (P,T) reduces - f, - g
then consider R being RedSequence of PolyRedRel (P,T) such that
A1: R . 1 = f and
A2: R . (len R) = g by REWRITE1:def 3;
defpred S₁[ Nat] means for q being Polynomial of n,L st q = R . $1 holds
PolyRedRel (P,T) reduces - f, - q;
A3: 1 <= len R by NAT_1:14;

A4: 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 A5: ( 1 <= k & k < len R ) ; :: thesis: ( S₁[k] implies S₁[k + 1] )
then 1 < len R by XXREAL_0:2;
then reconsider p = R . k as Polynomial of n,L by A5, Lm4;
assume S₁[k] ; :: thesis: S₁[k + 1]
then A6: PolyRedRel (P,T) reduces - f, - p ;

now :: thesis: for q being Polynomial of n,L st q = R . (k + 1) holds
PolyRedRel (P,T) reduces - f, - q

let q be Polynomial of n,L; :: thesis: ( q = R . (k + 1) implies PolyRedRel (P,T) reduces - f, - q )
assume A7: q = R . (k + 1) ; :: thesis: PolyRedRel (P,T) reduces - f, - q
( 1 <= k + 1 & k + 1 <= len R ) by A5, NAT_1:13;
then A8: k + 1 in dom R by FINSEQ_3:25;
k in dom R by A5, FINSEQ_3:25;
then [(R . k),(R . (k + 1))] in PolyRedRel (P,T) by A8, REWRITE1:def 2;
then p reduces_to q,P,T by A7, POLYRED:def 13;
then consider l being Polynomial of n,L such that
A9: l in P and
A10: p reduces_to q,l,T by POLYRED:def 7;
- p reduces_to - q,l,T by A10, Th45;
then - p reduces_to - q,P,T by A9, POLYRED:def 7;
then [(- p),(- q)] in PolyRedRel (P,T) by POLYRED:def 13;
then PolyRedRel (P,T) reduces - p, - q by REWRITE1:15;
hence PolyRedRel (P,T) reduces - f, - q by A6, REWRITE1:16; :: thesis: verum

end;

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

end;

A11: S₁[1] by A1, REWRITE1:12;
for i being Element of NAT st 1 <= i & i <= len R holds
S₁[i] from INT_1:sch 7(A11, A4);
hence PolyRedRel (P,T) reduces - f, - g by A2, A3; :: thesis: verum