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_{1}[ 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);

A23: for x being Element of the carrier of (Polynom-Ring ((n + 1),R)) holds S_{1}[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)

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

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

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_{1}[x,y]

consider P being Function of the carrier of (Polynom-Ring ((n + 1),R)), the carrier of (Polynom-Ring (Polynom-Ring (n,R))) such that 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_{1}[x,y]

reconsider p1 = x as Polynomial of (n + 1),R by POLYNOM1:def 11;

defpred S_{2}[ 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);

A16: for x being Element of NAT holds S_{2}[x,p3 . x]
from FUNCT_2:sch 3(A2);

reconsider p3 = p3 as sequence of (Polynom-Ring (n,R)) ;

take y = y; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A16; :: thesis: verum

end;reconsider p1 = x as Polynomial of (n + 1),R by POLYNOM1:def 11;

defpred S

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_{2}[i,p29]

consider p3 being sequence of the carrier of (Polynom-Ring (n,R)) such that let i be Element of NAT ; :: thesis: ex p29 being Element of the carrier of (Polynom-Ring (n,R)) st S_{2}[i,p29]

deffunc H_{1}( 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_{1}(b)
from FUNCT_2:sch 4();

reconsider p2 = p2 as Function of (Bags n),R ;

reconsider p2 = p2 as Series of n,R ;

then reconsider p29 = p2 as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def 11;

take p29 = p29; :: thesis: S_{2}[i,p29]

_{2}[i,p29]
; :: thesis: verum

end;deffunc H

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

reconsider p2 = p2 as Function of (Bags n),R ;

reconsider p2 = p2 as Series of n,R ;

now :: thesis: Support p2 is finite end;

then
p2 is finite-Support
by POLYNOM1:def 5;per cases
( Support p1 = {} or Support p2 = {} or ( Support p1 <> {} & Support p2 <> {} ) )
;

end;

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

end;

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

hence
Support p2 is finite
by A4; :: thesis: verumassume
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;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

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_{3}[ Element of Supportp2, set ] means $2 = $1 bag_extend i;

A8: for x being Element of Supportp2 holds S_{3}[x,f . x]
from FUNCT_2:sch 3(A7);

A9: dom f = Supportp2 by FUNCT_2:def 1;

rng f c= Supportp1 ;

then card Supportp2 c= card Supportp1 by A9, A14, CARD_1:10;

hence Support p2 is finite ; :: thesis: verum

end;reconsider Supportp1 = Support p1 as non empty Subset of (Bags (n + 1)) by A6;

defpred S

A7: now :: thesis: for x being Element of Supportp2 ex y being Element of Supportp1 st S_{3}[x,y]

consider f being Function of Supportp2,Supportp1 such that let x be Element of Supportp2; :: thesis: ex y being Element of Supportp1 st S_{3}[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_{3}[x,y]
; :: thesis: verum

end;( 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

A8: for x being Element of Supportp2 holds S

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

then A14:
f is one-to-one
by FUNCT_1:def 4;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;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

rng f c= Supportp1 ;

then card Supportp2 c= card Supportp1 by A9, A14, CARD_1:10;

hence Support p2 is finite ; :: thesis: verum

then reconsider p29 = p2 as Element of the carrier of (Polynom-Ring (n,R)) by POLYNOM1:def 11;

take p29 = p29; :: thesis: S

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)

hence
Sfor 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;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

A16: for x being Element of NAT holds S

reconsider p3 = p3 as sequence of (Polynom-Ring (n,R)) ;

now :: thesis: p3 is finite-Support end;

then reconsider y = p3 as Element of the carrier of (Polynom-Ring (Polynom-Ring (n,R))) by POLYNOM3:def 10;per cases
( Support p1 = {} or Support p1 <> {} )
;

end;

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

end;

now :: thesis: for i being Nat st i >= 0 holds

p3 . i = 0. (Polynom-Ring (n,R))

hence
p3 is finite-Support
by ALGSEQ_1:def 1; :: thesis: verump3 . 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;

hence p3 . i = 0_ (n,R) by POLYNOM1:def 8

.= 0. (Polynom-Ring (n,R)) by POLYNOM1:def 11 ;

:: thesis: verum

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

p2 = (Bags n) --> (0. R)
by A18;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;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

hence p3 . i = 0_ (n,R) by POLYNOM1:def 8

.= 0. (Polynom-Ring (n,R)) by POLYNOM1:def 11 ;

:: thesis: verum

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

then reconsider Supportp1 = Support p1 as non empty finite Subset of (Bags (n + 1)) ;

deffunc H_{1}( 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_{1}(x)
from FUNCT_2:sch 4();

reconsider j = max (f .: Supportp1) as Element of NAT by ORDINAL1:def 12;

end;deffunc H

consider f being Function of (Bags (n + 1)),NAT such that

A19: for x being Element of Bags (n + 1) holds f . x = H

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

hence
p3 is finite-Support
by ALGSEQ_1:def 1; :: thesis: verump3 . 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))

hence p3 . i = 0_ (n,R) by POLYNOM1:def 8

.= 0. (Polynom-Ring (n,R)) by POLYNOM1:def 11 ;

:: thesis: verum

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

p2 = (Bags n) --> (0. R)
by A21;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;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

hence p3 . i = 0_ (n,R) by POLYNOM1:def 8

.= 0. (Polynom-Ring (n,R)) by POLYNOM1:def 11 ;

:: thesis: verum

take y = y; :: thesis: S

thus S

A23: for x being Element of the carrier of (Polynom-Ring ((n + 1),R)) holds S

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)

hence
for p1 being Polynomial of (n + 1),Rfor 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;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

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