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));
set CPNR = the carrier of (Polynom-Ring (n,R));
defpred S₁[ Element of the carrier of (Polynom-Ring ((n + 1),R)), Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R)))] means for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p1 = $1 & p3 = $2 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i);

A1: now :: thesis: for x being Element of the carrier of (Polynom-Ring ((n + 1),R)) ex y being Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) st S₁[x,y]

let x be Element of the carrier of (Polynom-Ring ((n + 1),R)); :: thesis: ex y being Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) st S₁[x,y]
reconsider p1 = x as Polynomial of (n + 1),R by POLYNOM1:def 11;
defpred S₂[ Element of NAT , Element of the carrier of (Polynom-Ring (n,R))] means for p2 being Polynomial of n,R
for b being bag of n st p2 = $2 holds
p2 . b = p1 . (b bag_extend $1);

A2: now :: thesis: for i being Element of NAT ex p29 being Element of the carrier of (Polynom-Ring (n,R)) st S₂[i,p29]

let i be Element of NAT ; :: thesis: ex p29 being Element of the carrier of (Polynom-Ring (n,R)) st S₂[i,p29]
deffunc H₁( Element of Bags n) -> Element of the carrier of R = p1 . ($1 bag_extend i);
consider p2 being Function of (Bags n), the carrier of R such that
A3: for b being Element of Bags n holds p2 . b = H₁(b) from FUNCT_2:sch 4();
reconsider p2 = p2 as Function of (Bags n),R ;
reconsider p2 = p2 as Series of n,R ;

now :: thesis: Support p2 is finite

per cases ( Support p1 = {} or Support p2 = {} or ( Support p1 <> {} & Support p2 <> {} ) ) ;

suppose A4: Support p1 = {} ; :: thesis: Support p2 is finite

now :: thesis: ( Support p2 <> {} implies Support p1 <> {} )

assume Support p2 <> {} ; :: thesis: Support p1 <> {}
then consider b being object such that
A5: b in Support p2 by XBOOLE_0:def 1;
reconsider b = b as Element of Bags n by A5;
p2 . b <> 0. R by A5, POLYNOM1:def 4;
then p1 . (b bag_extend i) <> 0. R by A3;
hence Support p1 <> {} by POLYNOM1:def 4; :: thesis: verum

end;

hence Support p2 is finite by A4; :: thesis: verum

end;

suppose Support p2 = {} ; :: thesis: Support p2 is finite

hence Support p2 is finite ; :: thesis: verum

end;

suppose A6: ( Support p1 <> {} & Support p2 <> {} ) ; :: thesis: Support p2 is finite

then reconsider Supportp2 = Support p2 as non empty Subset of (Bags n) ;
reconsider Supportp1 = Support p1 as non empty Subset of (Bags (n + 1)) by A6;
defpred S₃[ Element of Supportp2, set ] means $2 = $1 bag_extend i;

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

let x be Element of Supportp2; :: thesis: ex y being Element of Supportp1 st S₃[x,y]
( x is Element of Bags n & p2 . x <> 0. R ) by POLYNOM1:def 4;
then p1 . (x bag_extend i) <> 0. R by A3;
then x bag_extend i in Support p1 by POLYNOM1:def 4;
hence ex y being Element of Supportp1 st S₃[x,y] ; :: thesis: verum

end;

consider f being Function of Supportp2,Supportp1 such that
A8: for x being Element of Supportp2 holds S₃[x,f . x] from FUNCT_2:sch 3(A7);
A9: dom f = Supportp2 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
A10: x1 in dom f and
A11: x2 in dom f and
A12: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x19 = x1, x29 = x2 as Element of Bags n by A9, A10, A11;
A13: x19 bag_extend i = f . x1 by A8, A10
.= x29 bag_extend i by A8, A11, A12 ;
x19 = (x19 bag_extend i) | n by Def1
.= x29 by A13, Def1 ;
hence x1 = x2 ; :: thesis: verum

end;

then A14: f is one-to-one by FUNCT_1:def 4;
rng f c= Supportp1 ;
then card Supportp2 c= card Supportp1 by A9, A14, CARD_1:10;
hence Support p2 is finite ; :: thesis: verum

end;

end;

end;

then p2 is finite-Support by POLYNOM1:def 5;
then reconsider p29 = p2 as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def 11;
take p29 = p29; :: thesis: S₂[i,p29]

now :: thesis: for p299 being Polynomial of n,R
for b being bag of n st p299 = p29 holds
p299 . b = p1 . (b bag_extend i)

let p299 be Polynomial of n,R; :: thesis: for b being bag of n st p299 = p29 holds
p299 . b = p1 . (b bag_extend i)
let b be bag of n; :: thesis: ( p299 = p29 implies p299 . b = p1 . (b bag_extend i) )
A15: b is Element of Bags n by PRE_POLY:def 12;
assume p299 = p29 ; :: thesis: p299 . b = p1 . (b bag_extend i)
hence p299 . b = p1 . (b bag_extend i) by A3, A15; :: thesis: verum

end;

hence S₂[i,p29] ; :: thesis: verum

end;

consider p3 being sequence of the carrier of (Polynom-Ring (n,R)) such that
A16: for x being Element of NAT holds S₂[x,p3 . x] from FUNCT_2:sch 3(A2);
reconsider p3 = p3 as sequence of (Polynom-Ring (n,R)) ;

now :: thesis: p3 is finite-Support

per cases ( Support p1 = {} or Support p1 <> {} ) ;

suppose A17: Support p1 = {} ; :: thesis: p3 is finite-Support

now :: thesis: for i being Nat st i >= 0 holds
p3 . i = 0. (Polynom-Ring (n,R))

let i be Nat; :: thesis: ( i >= 0 implies p3 . i = 0. (Polynom-Ring (n,R)) )
assume i >= 0 ; :: thesis: p3 . i = 0. (Polynom-Ring (n,R))
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
reconsider p2 = p3 . i1 as Polynomial of n,R by POLYNOM1:def 11;

A18: now :: thesis: for x being object st x in Bags n holds
p2 . x = ((Bags n) --> (0. R)) . x

let x be object ; :: thesis: ( x in Bags n implies p2 . x = ((Bags n) --> (0. R)) . x )
assume x in Bags n ; :: thesis: p2 . x = ((Bags n) --> (0. R)) . x
then reconsider x9 = x as Element of Bags n ;
p1 . (x9 bag_extend i) = 0. R by A17, POLYNOM1:def 4;
then p2 . x9 = 0. R by A16;
hence p2 . x = ((Bags n) --> (0. R)) . x ; :: thesis: verum

end;

p2 = (Bags n) --> (0. R) by A18;
hence p3 . i = 0_ (n,R) by POLYNOM1:def 8
.= 0. (Polynom-Ring (n,R)) by POLYNOM1:def 11 ;
:: thesis: verum

end;

hence p3 is finite-Support by ALGSEQ_1:def 1; :: thesis: verum

end;

suppose Support p1 <> {} ; :: thesis: p3 is finite-Support

then reconsider Supportp1 = Support p1 as non empty finite Subset of (Bags (n + 1)) ;
deffunc H₁( Element of Bags (n + 1)) -> Element of omega = $1 . n;
consider f being Function of (Bags (n + 1)),NAT such that
A19: for x being Element of Bags (n + 1) holds f . x = H₁(x) from FUNCT_2:sch 4();
reconsider j = max (f .: Supportp1) as Element of NAT by ORDINAL1:def 12;

now :: thesis: for i being Nat st i >= j + 1 holds
p3 . i = 0. (Polynom-Ring (n,R))

let i be Nat; :: thesis: ( i >= j + 1 implies p3 . i = 0. (Polynom-Ring (n,R)) )
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
reconsider p2 = p3 . i1 as Polynomial of n,R by POLYNOM1:def 11;
assume A20: i >= j + 1 ; :: thesis: p3 . i = 0. (Polynom-Ring (n,R))

A21: now :: thesis: for x being object st x in Bags n holds
p2 . x = ((Bags n) --> (0. R)) . x

let x be object ; :: thesis: ( x in Bags n implies p2 . x = ((Bags n) --> (0. R)) . x )
assume x in Bags n ; :: thesis: p2 . x = ((Bags n) --> (0. R)) . x
then reconsider x9 = x as Element of Bags n ;
i > j by A20, NAT_1:13;
then A22: not i in f .: Supportp1 by XXREAL_2:def 8;
f . (x9 bag_extend i) = (x9 bag_extend i) . n by A19
.= i by Def1 ;
then not x9 bag_extend i in Supportp1 by A22, FUNCT_2:35;
then p1 . (x9 bag_extend i) = 0. R by POLYNOM1:def 4;
then p2 . x9 = 0. R by A16;
hence p2 . x = ((Bags n) --> (0. R)) . x ; :: thesis: verum

end;

p2 = (Bags n) --> (0. R) by A21;
hence p3 . i = 0_ (n,R) by POLYNOM1:def 8
.= 0. (Polynom-Ring (n,R)) by POLYNOM1:def 11 ;
:: thesis: verum

end;

hence p3 is finite-Support by ALGSEQ_1:def 1; :: thesis: verum

end;

end;

end;

then reconsider y = p3 as Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) by POLYNOM3:def 10;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] by A16; :: thesis: verum

end;

consider P being Function of the carrier of (Polynom-Ring ((n + 1),R)), the carrier of (Polynom-Ring (Polynom-Ring (n,R))) such that
A23: for x being Element of the carrier of (Polynom-Ring ((n + 1),R)) holds S₁[x,P . x] from FUNCT_2:sch 3(A1);
reconsider P = P as Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) ;
take P ; :: thesis: for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)

now :: thesis: for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)

let p1 be Polynomial of (n + 1),R; :: thesis: for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
let p2 be Polynomial of n,R; :: thesis: for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
let p3 be Polynomial of (Polynom-Ring (n,R)); :: thesis: for i being Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
let i be Element of NAT ; :: thesis: for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i)
let b be bag of n; :: thesis: ( p3 = P . p1 & p2 = p3 . i implies p2 . b = p1 . (b bag_extend i) )
A24: p1 in the carrier of (Polynom-Ring ((n + 1),R)) by POLYNOM1:def 11;
assume ( p3 = P . p1 & p2 = p3 . i ) ; :: thesis: p2 . b = p1 . (b bag_extend i)
hence p2 . b = p1 . (b bag_extend i) by A23, A24; :: thesis: verum

end;

hence for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) ; :: thesis: verum