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

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 27;
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

let i be Element of NAT ; :: thesis: ex p2' being Element of the carrier of (Polynom-Ring n,R) st S₂[i,p2']
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

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

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

now

assume Support p2 <> {} ; :: thesis: Support p1 <> {}
then consider b being set 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 9;
then p1 . (b bag_extend i) <> 0. R by A3;
hence Support p1 <> {} by POLYNOM1:def 9; :: 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 ;
reconsider Supportp1 = Support p1 as non empty Subset of by A6;
defpred S₃[ Element of Supportp2, set ] means $2 = $1 bag_extend i;

A7: now

let x be Element of Supportp2; :: thesis: ex y being Element of Supportp1 st S₃[x,y]
x in Support p2 ;
then ( x is Element of Bags n & p2 . x <> 0. R ) by POLYNOM1:def 9, PRE_POLY:def 12;
then p1 . (x bag_extend i) <> 0. R by A3;
then x bag_extend i in Support p1 by POLYNOM1:def 9;
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

let x1, x2 be set ; :: 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 x1' = x1, x2' = x2 as Element of Bags n by A9, A10, A11;
A13: x1' bag_extend i = f . x1 by A8, A10
.= x2' bag_extend i by A8, A11, A12 ;
x1' = (x1' bag_extend i) | n by Def1
.= x2' by A13, Def1 ;
hence x1 = x2 ; :: thesis: verum

end;

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

end;

end;

end;

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

now

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

end;

hence S₂[i,p2'] ; :: thesis: verum

end;

consider p3 being Function of NAT ,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

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

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

now

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 13;
reconsider p2 = p3 . i1 as Polynomial of n,R by POLYNOM1:def 27;

A18: now

let x be set ; :: 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 x' = x as Element of Bags n ;
p1 . (x' bag_extend i) = 0. R by A17, POLYNOM1:def 9;
then p2 . x' = 0. R by A16;
hence p2 . x = ((Bags n) --> (0. R)) . x by FUNCOP_1:13; :: thesis: verum

end;

( dom ((Bags n) --> (0. R)) = Bags n & dom p2 = Bags n ) by FUNCOP_1:19, FUNCT_2:def 1;
then p2 = (Bags n) --> (0. R) by A18, FUNCT_1:9;
hence p3 . i = 0_ n,R by POLYNOM1:def 24
.= 0. (Polynom-Ring n,R) by POLYNOM1:def 27 ;
:: thesis: verum

end;

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

end;

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

then reconsider Supportp1 = Support p1 as non empty finite Subset of ;
deffunc H₁( Element of Bags (n + 1)) -> Element of NAT = $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 13;

now

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 13;
reconsider p2 = p3 . i1 as Polynomial of n,R by POLYNOM1:def 27;
assume A20: i >= j + 1 ; :: thesis: p3 . i = 0. (Polynom-Ring n,R)

A21: now

let x be set ; :: 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 x' = 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 . (x' bag_extend i) = (x' bag_extend i) . n by A19
.= i by Def1 ;
then not x' bag_extend i in Supportp1 by A22, FUNCT_2:43;
then p1 . (x' bag_extend i) = 0. R by POLYNOM1:def 9;
then p2 . x' = 0. R by A16;
hence p2 . x = ((Bags n) --> (0. R)) . x by FUNCOP_1:13; :: thesis: verum

end;

( dom ((Bags n) --> (0. R)) = Bags n & dom p2 = Bags n ) by FUNCOP_1:19, FUNCT_2:def 1;
then p2 = (Bags n) --> (0. R) by A21, FUNCT_1:9;
hence p3 . i = 0_ n,R by POLYNOM1:def 24
.= 0. (Polynom-Ring n,R) by POLYNOM1:def 27 ;
:: thesis: verum

end;

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

end;

end;

end;

then reconsider y = p3 as Element of the carrier of (Polynom-Ring (Polynom-Ring n,R)) by POLYNOM3:def 12;
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

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 27;
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