let n be Ordinal; 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 P being Subset of (Polynom-Ring (n,L))
for a, b being object st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )
let T be 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 P being Subset of (Polynom-Ring (n,L))
for a, b being object st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b 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 ; for P being Subset of (Polynom-Ring (n,L))
for a, b being object st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )
let P be Subset of (Polynom-Ring (n,L)); for a, b being object st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )
let f, g be object ; ( f <> g & PolyRedRel (P,T) reduces f,g implies ( f is Polynomial of n,L & g is Polynomial of n,L ) )
set R = PolyRedRel (P,T);
assume A1:
f <> g
; ( not PolyRedRel (P,T) reduces f,g or ( f is Polynomial of n,L & g is Polynomial of n,L ) )
assume
PolyRedRel (P,T) reduces f,g
; ( f is Polynomial of n,L & g is Polynomial of n,L )
then consider p being RedSequence of PolyRedRel (P,T) such that
A2:
p . 1 = f
and
A3:
p . (len p) = g
by REWRITE1:def 3;
reconsider l = (len p) - 1 as Element of NAT by INT_1:5, NAT_1:14;
set q = p . (1 + 1);
set h = p . l;
A4:
1 <= len p
by NAT_1:14;
now ( ( len p = 1 & f is Polynomial of n,L ) or ( len p <> 1 & f is Polynomial of n,L ) )per cases
( len p = 1 or len p <> 1 )
;
case
len p <> 1
;
f is Polynomial of n,Lthen
1
< len p
by A4, XXREAL_0:1;
then
1
+ 1
<= len p
by NAT_1:13;
then
1
+ 1
in Seg (len p)
by FINSEQ_1:1;
then A5:
1
+ 1
in dom p
by FINSEQ_1:def 3;
1
in Seg (len p)
by A4, FINSEQ_1:1;
then
1
in dom p
by FINSEQ_1:def 3;
then
[f,(p . (1 + 1))] in PolyRedRel (
P,
T)
by A2, A5, REWRITE1:def 2;
then consider h9,
g9 being
object such that A6:
[f,(p . (1 + 1))] = [h9,g9]
and A7:
h9 in NonZero (Polynom-Ring (n,L))
and
g9 in the
carrier of
(Polynom-Ring (n,L))
by RELSET_1:2;
f = h9
by A6, XTUPLE_0:1;
hence
f is
Polynomial of
n,
L
by A7, POLYNOM1:def 11;
verum end;
hence
f is Polynomial of n,L
; g is Polynomial of n,L
1 <= l + 1
by NAT_1:12;
then
l + 1 in Seg (len p)
by FINSEQ_1:1;
then A8:
l + 1 in dom p
by FINSEQ_1:def 3;
now ( ( len p = 1 & g is Polynomial of n,L ) or ( len p <> 1 & g is Polynomial of n,L ) )per cases
( len p = 1 or len p <> 1 )
;
case
len p <> 1
;
g is Polynomial of n,Lthen
0 + 1
< l + 1
by A4, XXREAL_0:1;
then A9:
1
<= l
by NAT_1:13;
l <= l + 1
by NAT_1:13;
then
l in Seg (len p)
by A9, FINSEQ_1:1;
then
l in dom p
by FINSEQ_1:def 3;
then
[(p . l),g] in PolyRedRel (
P,
T)
by A3, A8, REWRITE1:def 2;
then consider h9,
g9 being
object such that A10:
[(p . l),g] = [h9,g9]
and
h9 in NonZero (Polynom-Ring (n,L))
and A11:
g9 in the
carrier of
(Polynom-Ring (n,L))
by RELSET_1:2;
g = g9
by A10, XTUPLE_0:1;
hence
g is
Polynomial of
n,
L
by A11, POLYNOM1:def 11;
verum end;
hence
g is Polynomial of n,L
; verum