set CR = the carrier of R;
set PNR = Polynom-Ring (n,R);
set PN1R = Polynom-Ring ((n + 1),R);
set PRPNR = Polynom-Ring (Polynom-Ring (n,R));
set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R)));
set CPN1R = the carrier of (Polynom-Ring ((n + 1),R));
defpred S1[ Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))), Element of the carrier of (Polynom-Ring ((n + 1),R))] means for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p1 = $1 & p3 = $2 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n);
A1:
now for x being Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) ex y being Element of the carrier of (Polynom-Ring ((n + 1),R)) st S1[x,y]let x be
Element of the
carrier of
(Polynom-Ring (Polynom-Ring (n,R)));
ex y being Element of the carrier of (Polynom-Ring ((n + 1),R)) st S1[x,y]reconsider p1 =
x as
Polynomial of
(Polynom-Ring (n,R)) by POLYNOM3:def 10;
defpred S2[
Element of
Bags (n + 1),
Element of the
carrier of
R]
means for
p2 being
Polynomial of
n,
R st
p2 = p1 . ($1 . n) holds
$2
= p2 . ($1 | n);
deffunc H1(
object )
-> set =
{ b where b is Element of Bags (n + 1) : ( b . n = $1 & ( for p2 being Polynomial of n,R st p2 = p1 . $1 holds
b | n in Support p2 ) ) } ;
consider A being
sequence of
(bool (Bags (n + 1))) such that A3:
for
k being
object st
k in NAT holds
A . k = H1(
k)
from FUNCT_2:sch 2(A2);
now for X being set st X in A .: (len p1) holds
X is finite let X be
set ;
( X in A .: (len p1) implies b1 is finite )assume
X in A .: (len p1)
;
b1 is finite then consider k being
Element of
NAT such that
k in len p1
and A4:
X = A . k
by FUNCT_2:65;
reconsider p2 =
p1 . k as
Polynomial of
n,
R by POLYNOM1:def 11;
A5:
A . k = { b where b is Element of Bags (n + 1) : ( b . n = k & ( for p2 being Polynomial of n,R st p2 = p1 . k holds
b | n in Support p2 ) ) }
by A3;
per cases
( Support p2 = {} or Support p2 <> {} )
;
suppose A8:
Support p2 <> {}
;
b1 is finite then consider b2 being
object such that A9:
b2 in Support p2
by XBOOLE_0:def 1;
reconsider b2 =
b2 as
Element of
Bags n by A9;
A10:
(b2 bag_extend k) . n = k
by Def1;
for
p2 being
Polynomial of
n,
R st
p2 = p1 . k holds
(b2 bag_extend k) | n in Support p2
by A9, Def1;
then
b2 bag_extend k in A . k
by A5, A10;
then reconsider Ak =
A . k as non
empty set ;
reconsider Supportp2 =
Support p2 as non
empty set by A8;
defpred S3[
Element of
Ak,
Element of
Supportp2]
means for
b being
Element of
Bags (n + 1) st $1
= b holds
$2
= b | n;
consider f being
Function of
Ak,
Supportp2 such that A14:
for
x being
Element of
Ak holds
S3[
x,
f . x]
from FUNCT_2:sch 3(A11);
A15:
dom f = Ak
by FUNCT_2:def 1;
now for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume that A16:
x1 in dom f
and A17:
x2 in dom f
and A18:
f . x1 = f . x2
;
x1 = x2
f . x1 in Supportp2
by A16, FUNCT_2:5;
then reconsider fx1 =
f . x1 as
Element of
Bags n ;
consider b1 being
Element of
Bags (n + 1) such that A19:
b1 = x1
and A20:
b1 . n = k
and
for
p2 being
Polynomial of
n,
R st
p2 = p1 . k holds
b1 | n in Support p2
by A5, A15, A16;
b1 | n = f . x1
by A14, A16, A19;
then A21:
b1 = fx1 bag_extend k
by A20, Def1;
consider b2 being
Element of
Bags (n + 1) such that A22:
b2 = x2
and A23:
b2 . n = k
and
for
p2 being
Polynomial of
n,
R st
p2 = p1 . k holds
b2 | n in Support p2
by A5, A15, A17;
b2 | n = f . x1
by A14, A17, A18, A22;
hence
x1 = x2
by A19, A21, A22, A23, Def1;
verum end; then A24:
f is
one-to-one
by FUNCT_1:def 4;
rng f c= Supportp2
;
then
card Ak c= card Supportp2
by A15, A24, CARD_1:10;
hence
X is
finite
by A4;
verum end; end; end; then A25:
union (A .: (len p1)) is
finite
by FINSET_1:7;
consider y being
Function of
(Bags (n + 1)), the
carrier of
R such that A27:
for
b being
Element of
Bags (n + 1) holds
S2[
b,
y . b]
from FUNCT_2:sch 3(A26);
reconsider y =
y as
Function of
(Bags (n + 1)),
R ;
reconsider y =
y as
Series of
(n + 1),
R ;
Support y c= union (A .: (len p1))
then
y is
finite-Support
by A25, POLYNOM1:def 5;
then reconsider y9 =
y as
Element of the
carrier of
(Polynom-Ring ((n + 1),R)) by POLYNOM1:def 11;
hence
ex
y being
Element of the
carrier of
(Polynom-Ring ((n + 1),R)) st
S1[
x,
y]
;
verum end;
consider P being Function of the carrier of (Polynom-Ring (Polynom-Ring (n,R))), the carrier of (Polynom-Ring ((n + 1),R)) such that
A35:
for x being Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) holds S1[x,P . x]
from FUNCT_2:sch 3(A1);
reconsider P = P as Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) ;
take
P
; for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
hence
for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
; verum