let n be Ordinal; for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for g being set
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; for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for g being set
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 associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; for f being Polynomial of n,L
for g being set
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; for g being set
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 set ; 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)); ( 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
; 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;
A4:
1 <= len p
by NAT_1:14;
reconsider l = (len p) - 1 as Element of NAT by INT_1:18, NAT_1:14;
set h = p . l;
1 <= l + 1
by NAT_1:12;
then
l + 1 in Seg (len p)
by FINSEQ_1:3;
then A5:
l + 1 in dom p
by FINSEQ_1:def 3;
per cases
( len p = 1 or len p <> 1 )
;
suppose
len p <> 1
;
g is Polynomial of n,Lthen
0 + 1
< l + 1
by A4, XXREAL_0:1;
then A6:
1
<= l
by NAT_1:13;
l <= l + 1
by NAT_1:13;
then
l in Seg (len p)
by A6, FINSEQ_1:3;
then
l in dom p
by FINSEQ_1:def 3;
then
[(p . l),g] in PolyRedRel (
P,
T)
by A2, A5, REWRITE1:def 2;
then consider h9,
g9 being
set such that A7:
[(p . l),g] = [h9,g9]
and
h9 in NonZero (Polynom-Ring (n,L))
and A8:
g9 in the
carrier of
(Polynom-Ring (n,L))
by RELSET_1:6;
g =
[h9,g9] `2
by A7, MCART_1:def 2
.=
g9
by MCART_1:def 2
;
hence
g is
Polynomial of
n,
L
by A8, POLYNOM1:def 27;
verum end;