set PRPNR = Polynom-Ring (Polynom-Ring n,R);
set PN1R = Polynom-Ring (n + 1),R;
set PNR = 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);
set CR = the carrier of 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 st p1 = $1 & p3 = $2 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n);
A1:
now let x be
Element of the
carrier of
(Polynom-Ring (Polynom-Ring n,R));
:: thesis: 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 12;
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);
consider y being
Function of
(Bags (n + 1)),the
carrier of
R such that A3:
for
b being
Element of
Bags (n + 1) holds
S2[
b,
y . b]
from FUNCT_2:sch 3(A2);
reconsider y =
y as
Function of
(Bags (n + 1)),
R ;
reconsider y =
y as
Series of
(n + 1),
R ;
deffunc H1(
set )
-> 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
Function of
NAT ,
(bool (Bags (n + 1))) such that A6:
for
k being
set st
k in NAT holds
A . k = H1(
k)
from FUNCT_2:sch 2(A4);
now let X be
set ;
:: thesis: ( X in A .: (len p1) implies b1 is finite )assume
X in A .: (len p1)
;
:: thesis: b1 is finite then consider k being
Element of
NAT such that A7:
(
k in len p1 &
X = A . k )
by FUNCT_2:116;
A8:
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 A6;
reconsider p2 =
p1 . k as
Polynomial of
n,
R by POLYNOM1:def 27;
per cases
( Support p2 = {} or Support p2 <> {} )
;
suppose A12:
Support p2 <> {}
;
:: thesis: b1 is finite then consider b2 being
set such that A13:
b2 in Support p2
by XBOOLE_0:def 1;
reconsider b2 =
b2 as
Element of
Bags n by A13;
A14:
(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 A13, Def1;
then
b2 bag_extend k in A . k
by A8, A14;
then reconsider Ak =
A . k as non
empty set ;
reconsider Supportp2 =
Support p2 as non
empty set by A12;
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 A17:
for
x being
Element of
Ak holds
S3[
x,
f . x]
from FUNCT_2:sch 3(A15);
A18:
dom f = Ak
by FUNCT_2:def 1;
now let x1,
x2 be
set ;
:: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume A19:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
:: thesis: x1 = x2then consider b1 being
Element of
Bags (n + 1) such that A20:
(
b1 = x1 &
b1 . n = k & ( for
p2 being
Polynomial of
n,
R st
p2 = p1 . k holds
b1 | n in Support p2 ) )
by A8, A18;
f . x1 in Supportp2
by A19, FUNCT_2:7;
then reconsider fx1 =
f . x1 as
Element of
Bags n ;
b1 | n = f . x1
by A17, A19, A20;
then A21:
b1 = fx1 bag_extend k
by A20, Def1;
consider b2 being
Element of
Bags (n + 1) such that A22:
(
b2 = x2 &
b2 . n = k & ( for
p2 being
Polynomial of
n,
R st
p2 = p1 . k holds
b2 | n in Support p2 ) )
by A8, A18, A19;
b2 | n = f . x1
by A17, A19, A22;
hence
x1 = x2
by A20, A21, A22, Def1;
:: thesis: verum end; then A23:
f is
one-to-one
by FUNCT_1:def 8;
rng f c= Supportp2
;
then
card Ak c= card Supportp2
by A18, A23, CARD_1:26;
hence
X is
finite
by A7;
:: thesis: verum end; end; then A24:
union (A .: (len p1)) is
finite
by FINSET_1:25;
Support y c= union (A .: (len p1))
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Support y or x in union (A .: (len p1)) )
assume A25:
x in Support y
;
:: thesis: x in union (A .: (len p1))
then reconsider x' =
x as
Element of
Bags (n + 1) ;
A26:
y . x' <> 0. R
by A25, POLYNOM1:def 9;
reconsider p2 =
p1 . (x' . n) as
Polynomial of
n,
R by POLYNOM1:def 27;
n < n + 1
by XREAL_1:31;
then reconsider xn =
x' | n as
Element of
Bags n by Th3;
A27:
p2 . xn <> 0. R
by A3, A26;
then A28:
for
p2 being
Polynomial of
n,
R st
p2 = p1 . (x' . n) holds
xn in Support p2
by POLYNOM1:def 9;
A . (x' . n) = { b where b is Element of Bags (n + 1) : ( b . n = x' . n & ( for p2 being Polynomial of n,R st p2 = p1 . (x' . n) holds
b | n in Support p2 ) ) }
by A6;
then A29:
x in A . (x' . n)
by A28;
p2 <> 0_ n,
R
by A27, POLYNOM1:81;
then
p2 <> 0. (Polynom-Ring n,R)
by POLYNOM1:def 27;
then A30:
x' . n < len p1
by ALGSEQ_1:22;
len p1 = { i where i is Element of NAT : i < len p1 }
by AXIOMS:30;
then A31:
x' . n in len p1
by A30;
dom A = NAT
by FUNCT_2:def 1;
then
A . (x' . n) in A .: (len p1)
by A31, FUNCT_1:def 12;
hence
x in union (A .: (len p1))
by A29, TARSKI:def 4;
:: thesis: verum
end; then
Support y is
finite
by A24;
then
y is
finite-Support
by POLYNOM1:def 10;
then reconsider y' =
y as
Element of the
carrier of
(Polynom-Ring (n + 1),R) by POLYNOM1:def 27;
hence
ex
y being
Element of the
carrier of
(Polynom-Ring (n + 1),R) st
S1[
x,
y]
;
:: thesis: 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
A33:
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
; :: thesis: 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 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 st p3 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
; :: thesis: verum