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_{1}[ 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;

_{1}[1]
by A1, REWRITE1:12;

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

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

hence PolyRedRel (P,T) reduces - f, - g by A2, A3; :: thesis: verum

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

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_{1}[k] holds

S_{1}[k + 1]

A11:
SS

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

assume A5: ( 1 <= k & k < len R ) ; :: thesis: ( S_{1}[k] implies S_{1}[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_{1}[k]
; :: thesis: S_{1}[k + 1]

then A6: PolyRedRel (P,T) reduces - f, - p ;

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

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

then 1 < len R by XXREAL_0:2;

then reconsider p = R . k as Polynomial of n,L by A5, Lm4;

assume S

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

hence
SPolyRedRel (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;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

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

S

hence PolyRedRel (P,T) reduces - f, - g by A2, A3; :: thesis: verum