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 S₁[ 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 :: thesis: 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 S₁[x,y]

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 S₁[x,y]
reconsider p1 = x as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def 10;
defpred S₂[ 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 H₁( 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 ) ) } ;

A2: now :: thesis: for k being object st k in NAT holds
H₁(k) in bool (Bags (n + 1))

let k be object ; :: thesis: ( k in NAT implies H₁(k) in bool (Bags (n + 1)) )
assume k in NAT ; :: thesis: H₁(k) in bool (Bags (n + 1))
set Ak = H₁(k);
H₁(k) c= Bags (n + 1)

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in H₁(k) or b in Bags (n + 1) )
assume b in H₁(k) ; :: thesis: b in Bags (n + 1)
then ex b9 being Element of Bags (n + 1) st
( b9 = b & b9 . n = k & ( for p2 being Polynomial of n,R st p2 = p1 . k holds
b9 | n in Support p2 ) ) ;
hence b in Bags (n + 1) ; :: thesis: verum

end;

hence H₁(k) in bool (Bags (n + 1)) ; :: thesis: verum

end;

consider A being sequence of (bool (Bags (n + 1))) such that
A3: for k being object st k in NAT holds
A . k = H₁(k) from FUNCT_2:sch 2(A2);

now :: thesis: for X being set st X in A .: (len p1) holds
X is finite

let X be set ; :: thesis: ( X in A .: (len p1) implies b₁ is finite )
assume X in A .: (len p1) ; :: thesis: b₁ 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 A6: Support p2 = {} ; :: thesis: b₁ is finite

now :: thesis: not A . k <> {}

assume A . k <> {} ; :: thesis: contradiction
then consider b being object such that
A7: b in A . k by XBOOLE_0:def 1;
ex b9 being Element of Bags (n + 1) st
( b9 = b & b9 . n = k & ( for p2 being Polynomial of n,R st p2 = p1 . k holds
b9 | n in Support p2 ) ) by A5, A7;
hence contradiction by A6; :: thesis: verum

end;

hence X is finite by A4; :: thesis: verum

end;

suppose A8: Support p2 <> {} ; :: thesis: b₁ 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 S₃[ Element of Ak, Element of Supportp2] means for b being Element of Bags (n + 1) st $1 = b holds
$2 = b | n;

A11: now :: thesis: for x being Element of Ak ex y being Element of Supportp2 st S₃[x,y]

let x be Element of Ak; :: thesis: ex y being Element of Supportp2 st S₃[x,y]
x in A . k ;
then consider b being Element of Bags (n + 1) such that
A12: b = x and
b . n = k and
A13: for p2 being Polynomial of n,R st p2 = p1 . k holds
b | n in Support p2 by A5;
reconsider bn = b | n as Element of Supportp2 by A13;
S₃[x,bn] by A12;
hence ex y being Element of Supportp2 st S₃[x,y] ; :: thesis: verum

end;

consider f being Function of Ak,Supportp2 such that
A14: for x being Element of Ak holds S₃[x,f . x] from FUNCT_2:sch 3(A11);
A15: dom f = Ak by FUNCT_2:def 1;

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

end;

end;

then A25: union (A .: (len p1)) is finite by FINSET_1:7;

A26: now :: thesis: for b being Element of Bags (n + 1) ex r being Element of the carrier of R st S₂[b,r]

let b be Element of Bags (n + 1); :: thesis: ex r being Element of the carrier of R st S₂[b,r]
reconsider p2 = p1 . (b . n) as Polynomial of n,R by POLYNOM1:def 11;
n < n + 1 by XREAL_1:29;
then reconsider bn = b | n as bag of n by Th3;
S₂[b,p2 . bn] ;
hence ex r being Element of the carrier of R st S₂[b,r] ; :: thesis: verum

end;

consider y being Function of (Bags (n + 1)), the carrier of R such that
A27: for b being Element of Bags (n + 1) holds S₂[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))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Support y or x in union (A .: (len p1)) )
A28: dom A = NAT by FUNCT_2:def 1;
assume A29: x in Support y ; :: thesis: x in union (A .: (len p1))
then reconsider x9 = x as Element of Bags (n + 1) ;
reconsider p2 = p1 . (x9 . n) as Polynomial of n,R by POLYNOM1:def 11;
n < n + 1 by XREAL_1:29;
then reconsider xn = x9 | n as Element of Bags n by Th3;
y . x9 <> 0. R by A29, POLYNOM1:def 4;
then A30: p2 . xn <> 0. R by A27;
then p2 <> 0_ (n,R) by POLYNOM1:22;
then p2 <> 0. (Polynom-Ring (n,R)) by POLYNOM1:def 11;
then A31: x9 . n < len p1 by ALGSEQ_1:8;
len p1 = { i where i is Nat : i < len p1 } by AXIOMS:4;
then x9 . n in len p1 by A31;
then A32: A . (x9 . n) in A .: (len p1) by A28, FUNCT_1:def 6;
A33: A . (x9 . n) = { b where b is Element of Bags (n + 1) : ( b . n = x9 . n & ( for p2 being Polynomial of n,R st p2 = p1 . (x9 . n) holds
b | n in Support p2 ) ) } by A3;
for p2 being Polynomial of n,R st p2 = p1 . (x9 . n) holds
xn in Support p2 by A30, POLYNOM1:def 4;
then x in A . (x9 . n) by A33;
hence x in union (A .: (len p1)) by A32, TARSKI:def 4; :: thesis: verum

end;

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;

now :: 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 n + 1 st p1 = x & p3 = y9 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)

let p1 be Polynomial of (Polynom-Ring (n,R)); :: thesis: for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p1 = x & p3 = y9 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
let p2 be Polynomial of n,R; :: thesis: for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p1 = x & p3 = y9 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
let p3 be Polynomial of (n + 1),R; :: thesis: for b being bag of n + 1 st p1 = x & p3 = y9 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
let b be bag of n + 1; :: thesis: ( p1 = x & p3 = y9 & p2 = p1 . (b . n) implies p3 . b = p2 . (b | n) )
A34: b is Element of Bags (n + 1) by PRE_POLY:def 12;
assume ( p1 = x & p3 = y9 & p2 = p1 . (b . n) ) ; :: thesis: p3 . b = p2 . (b | n)
hence p3 . b = p2 . (b | n) by A27, A34; :: thesis: verum

end;

hence ex y being Element of the carrier of (Polynom-Ring ((n + 1),R)) st S₁[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
A35: for x being Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) holds S₁[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 n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)

now :: 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 n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)

let p1 be Polynomial of (Polynom-Ring (n,R)); :: thesis: 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)
let p2 be Polynomial of n,R; :: thesis: 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)
let p3 be Polynomial of (n + 1),R; :: thesis: for b being bag of n + 1 st p3 = P . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n)
let b be bag of n + 1; :: thesis: ( p3 = P . p1 & p2 = p1 . (b . n) implies p3 . b = p2 . (b | n) )
A36: p1 in the carrier of (Polynom-Ring (Polynom-Ring (n,R))) by POLYNOM3:def 10;
assume ( p3 = P . p1 & p2 = p1 . (b . n) ) ; :: thesis: p3 . b = p2 . (b | n)
hence p3 . b = p2 . (b | n) by A35, A36; :: thesis: verum

end;

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) ; :: thesis: verum