let n be Ordinal; :: thesis: for T being connected TermOrder of n

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

for f being Polynomial of n,L

for g being object

for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

g is Polynomial of n,L

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for f being Polynomial of n,L

for g being object

for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

g is Polynomial of n,L

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f being Polynomial of n,L

for g being object

for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

g is Polynomial of n,L

let f be Polynomial of n,L; :: thesis: for g being object

for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

g is Polynomial of n,L

let g be object ; :: thesis: for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

g is Polynomial of n,L

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( PolyRedRel (P,T) reduces f,g implies g is Polynomial of n,L )

set R = PolyRedRel (P,T);

assume PolyRedRel (P,T) reduces f,g ; :: thesis: g is Polynomial of n,L

then consider p being RedSequence of PolyRedRel (P,T) such that

A1: p . 1 = f and

A2: p . (len p) = g by REWRITE1:def 3;

A3: 1 <= len p by NAT_1:14;

reconsider l = (len p) - 1 as Element of NAT by INT_1:5, NAT_1:14;

set h = p . l;

1 <= l + 1 by NAT_1:12;

then l + 1 in Seg (len p) by FINSEQ_1:1;

then A4: l + 1 in dom p by FINSEQ_1:def 3;

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

for f being Polynomial of n,L

for g being object

for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

g is Polynomial of n,L

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for f being Polynomial of n,L

for g being object

for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

g is Polynomial of n,L

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f being Polynomial of n,L

for g being object

for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

g is Polynomial of n,L

let f be Polynomial of n,L; :: thesis: for g being object

for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

g is Polynomial of n,L

let g be object ; :: thesis: for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds

g is Polynomial of n,L

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( PolyRedRel (P,T) reduces f,g implies g is Polynomial of n,L )

set R = PolyRedRel (P,T);

assume PolyRedRel (P,T) reduces f,g ; :: thesis: g is Polynomial of n,L

then consider p being RedSequence of PolyRedRel (P,T) such that

A1: p . 1 = f and

A2: p . (len p) = g by REWRITE1:def 3;

A3: 1 <= len p by NAT_1:14;

reconsider l = (len p) - 1 as Element of NAT by INT_1:5, NAT_1:14;

set h = p . l;

1 <= l + 1 by NAT_1:12;

then l + 1 in Seg (len p) by FINSEQ_1:1;

then A4: l + 1 in dom p by FINSEQ_1:def 3;

per cases
( len p = 1 or len p <> 1 )
;

end;

suppose
len p <> 1
; :: thesis: g is Polynomial of n,L

then
0 + 1 < l + 1
by A3, XXREAL_0:1;

then A5: 1 <= l by NAT_1:13;

l <= l + 1 by NAT_1:13;

then l in Seg (len p) by A5, FINSEQ_1:1;

then l in dom p by FINSEQ_1:def 3;

then [(p . l),g] in PolyRedRel (P,T) by A2, A4, REWRITE1:def 2;

then consider h9, g9 being object such that

A6: [(p . l),g] = [h9,g9] and

h9 in NonZero (Polynom-Ring (n,L)) and

A7: g9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;

g = g9 by A6, XTUPLE_0:1;

hence g is Polynomial of n,L by A7, POLYNOM1:def 11; :: thesis: verum

end;then A5: 1 <= l by NAT_1:13;

l <= l + 1 by NAT_1:13;

then l in Seg (len p) by A5, FINSEQ_1:1;

then l in dom p by FINSEQ_1:def 3;

then [(p . l),g] in PolyRedRel (P,T) by A2, A4, REWRITE1:def 2;

then consider h9, g9 being object such that

A6: [(p . l),g] = [h9,g9] and

h9 in NonZero (Polynom-Ring (n,L)) and

A7: g9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;

g = g9 by A6, XTUPLE_0:1;

hence g is Polynomial of n,L by A7, POLYNOM1:def 11; :: thesis: verum