set PNR = Polynom-Ring (n,R);

set PN1R = Polynom-Ring ((n + 1),R);

set PRPNR = Polynom-Ring (Polynom-Ring (n,R));

set CPN1R = the carrier of (Polynom-Ring ((n + 1),R));

let A, B be Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))); :: 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 = A . p1 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i) ) & ( 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 = B . p1 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i) ) implies A = B )

assume A25: 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 = A . p1 & p2 = p3 . i holds

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

( p3 = B . p1 & p2 = p3 . i & not p2 . b = p1 . (b bag_extend i) ) or A = B )

assume A26: 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 = B . p1 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i) ; :: thesis: A = B

set PN1R = Polynom-Ring ((n + 1),R);

set PRPNR = Polynom-Ring (Polynom-Ring (n,R));

set CPN1R = the carrier of (Polynom-Ring ((n + 1),R));

let A, B be Function of (Polynom-Ring ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))); :: 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 = A . p1 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i) ) & ( 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 = B . p1 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i) ) implies A = B )

assume A25: 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 = A . p1 & p2 = p3 . i holds

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

( p3 = B . p1 & p2 = p3 . i & not p2 . b = p1 . (b bag_extend i) ) or A = B )

assume A26: 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 = B . p1 & p2 = p3 . i holds

p2 . b = p1 . (b bag_extend i) ; :: thesis: A = B

now :: thesis: for x being object st x in the carrier of (Polynom-Ring ((n + 1),R)) holds

A . x = B . x

hence
A = B
; :: thesis: verumA . x = B . x

let x be object ; :: thesis: ( x in the carrier of (Polynom-Ring ((n + 1),R)) implies A . x = B . x )

assume A27: x in the carrier of (Polynom-Ring ((n + 1),R)) ; :: thesis: A . x = B . x

then reconsider x99 = x as Element of the carrier of (Polynom-Ring ((n + 1),R)) ;

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

reconsider Ax = A . x99, Bx = B . x99 as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def 10;

end;assume A27: x in the carrier of (Polynom-Ring ((n + 1),R)) ; :: thesis: A . x = B . x

then reconsider x99 = x as Element of the carrier of (Polynom-Ring ((n + 1),R)) ;

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

reconsider Ax = A . x99, Bx = B . x99 as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def 10;

now :: thesis: for i being object st i in NAT holds

Ax . i = Bx . i

hence
A . x = B . x
by FUNCT_2:12; :: thesis: verumAx . i = Bx . i

let i be object ; :: thesis: ( i in NAT implies Ax . i = Bx . i )

assume i in NAT ; :: thesis: Ax . i = Bx . i

then reconsider i9 = i as Element of NAT ;

reconsider Axi = Ax . i9, Bxi = Bx . i9 as Polynomial of n,R by POLYNOM1:def 11;

end;assume i in NAT ; :: thesis: Ax . i = Bx . i

then reconsider i9 = i as Element of NAT ;

reconsider Axi = Ax . i9, Bxi = Bx . i9 as Polynomial of n,R by POLYNOM1:def 11;

now :: thesis: for b being object st b in Bags n holds

Axi . b = Bxi . b

hence
Ax . i = Bx . i
by FUNCT_2:12; :: thesis: verumAxi . b = Bxi . b

let b be object ; :: thesis: ( b in Bags n implies Axi . b = Bxi . b )

assume b in Bags n ; :: thesis: Axi . b = Bxi . b

then reconsider b9 = b as bag of n ;

thus Axi . b = x9 . (b9 bag_extend i9) by A25

.= Bxi . b by A26 ; :: thesis: verum

end;assume b in Bags n ; :: thesis: Axi . b = Bxi . b

then reconsider b9 = b as bag of n ;

thus Axi . b = x9 . (b9 bag_extend i9) by A25

.= Bxi . b by A26 ; :: thesis: verum