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 S1[ 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 . ();
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 S1[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 S1[x,y]
reconsider p1 = x as Polynomial of (n + 1),R by POLYNOM1:def 11;
defpred S2[ 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 S2[i,p29]
let i be Element of NAT ; :: thesis: ex p29 being Element of the carrier of (Polynom-Ring (n,R)) st S2[i,p29]
deffunc H1( 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 = H1(b) from 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:
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 ;
then p1 . () <> 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 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 S3[ 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 S3[x,y]
let x be Element of Supportp2; :: thesis: ex y being Element of Supportp1 st S3[x,y]
( x is Element of Bags n & p2 . x <> 0. R ) by POLYNOM1:def 4;
then p1 . () <> 0. R by A3;
then x bag_extend i in Support p1 by POLYNOM1:def 4;
hence ex y being Element of Supportp1 st S3[x,y] ; :: thesis: verum
end;
consider f being Function of Supportp2,Supportp1 such that
A8: for x being Element of Supportp2 holds S3[x,f . x] from 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
.= x29 bag_extend i by A8, A11, A12 ;
x19 = (x19 bag_extend i) | n by Def1
.= x29 by ;
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 ;
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: S2[i,p29]
now :: thesis: for p299 being Polynomial of n,R
for b being bag of n st p299 = p29 holds
p299 . b = p1 . ()
let p299 be Polynomial of n,R; :: thesis: for b being bag of n st p299 = p29 holds
p299 . b = p1 . ()

let b be bag of n; :: thesis: ( p299 = p29 implies p299 . b = p1 . () )
A15: b is Element of Bags n by PRE_POLY:def 12;
assume p299 = p29 ; :: thesis: p299 . b = p1 . ()
hence p299 . b = p1 . () by ; :: thesis: verum
end;
hence S2[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 S2[x,p3 . x] from 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 ;
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 H1( 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 = H1(x) from 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 ;
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 ;
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: S1[x,y]
thus S1[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 S1[x,P . x] from 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 . ()

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 . ()
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 . ()

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 . ()

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 . ()

let i be Element of NAT ; :: thesis: for b being bag of n st p3 = P . p1 & p2 = p3 . i holds
p2 . b = p1 . ()

let b be bag of n; :: thesis: ( p3 = P . p1 & p2 = p3 . i implies p2 . b = p1 . () )
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 . ()
hence p2 . b = p1 . () by ; :: 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 . () ; :: thesis: verum