let A, B be Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)); :: thesis: ( ( for p1 being Polynomial of (Polynom-Ring (n,R))

for p2 being Polynomial of n,R

for p3 being Polynomial of (n + 1),R

for b being bag of n + 1 st p3 = A . p1 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n) ) & ( for p1 being Polynomial of (Polynom-Ring (n,R))

for p2 being Polynomial of n,R

for p3 being Polynomial of (n + 1),R

for b being bag of n + 1 st p3 = B . p1 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n) ) implies A = B )

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

set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R)));

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

assume A37: for p1 being Polynomial of (Polynom-Ring (n,R))

for p2 being Polynomial of n,R

for p3 being Polynomial of (n + 1),R

for b being bag of n + 1 st p3 = A . p1 & p2 = p1 . (b . n) holds

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

( p3 = B . p1 & p2 = p1 . (b . n) & not p3 . b = p2 . (b | n) ) or A = B )

assume A38: for p1 being Polynomial of (Polynom-Ring (n,R))

for p2 being Polynomial of n,R

for p3 being Polynomial of (n + 1),R

for b being bag of n + 1 st p3 = B . p1 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n) ; :: thesis: A = B

for p2 being Polynomial of n,R

for p3 being Polynomial of (n + 1),R

for b being bag of n + 1 st p3 = A . p1 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n) ) & ( for p1 being Polynomial of (Polynom-Ring (n,R))

for p2 being Polynomial of n,R

for p3 being Polynomial of (n + 1),R

for b being bag of n + 1 st p3 = B . p1 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n) ) implies A = B )

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

set CPRPNR = the carrier of (Polynom-Ring (Polynom-Ring (n,R)));

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

assume A37: for p1 being Polynomial of (Polynom-Ring (n,R))

for p2 being Polynomial of n,R

for p3 being Polynomial of (n + 1),R

for b being bag of n + 1 st p3 = A . p1 & p2 = p1 . (b . n) holds

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

( p3 = B . p1 & p2 = p1 . (b . n) & not p3 . b = p2 . (b | n) ) or A = B )

assume A38: for p1 being Polynomial of (Polynom-Ring (n,R))

for p2 being Polynomial of n,R

for p3 being Polynomial of (n + 1),R

for b being bag of n + 1 st p3 = B . p1 & p2 = p1 . (b . n) holds

p3 . b = p2 . (b | n) ; :: thesis: A = B

now :: thesis: for x being object st x in the carrier of (Polynom-Ring (Polynom-Ring (n,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 (Polynom-Ring (n,R))) implies A . x = B . x )

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

then reconsider x9 = x as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def 10;

( A . x in the carrier of (Polynom-Ring ((n + 1),R)) & B . x in the carrier of (Polynom-Ring ((n + 1),R)) ) by A39, FUNCT_2:5;

then reconsider Ax = A . x, Bx = B . x as Polynomial of (n + 1),R by POLYNOM1:def 11;

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

then reconsider x9 = x as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def 10;

( A . x in the carrier of (Polynom-Ring ((n + 1),R)) & B . x in the carrier of (Polynom-Ring ((n + 1),R)) ) by A39, FUNCT_2:5;

then reconsider Ax = A . x, Bx = B . x as Polynomial of (n + 1),R by POLYNOM1:def 11;

now :: thesis: for b being object st b in Bags (n + 1) holds

Ax . b = Bx . b

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

let b be object ; :: thesis: ( b in Bags (n + 1) implies Ax . b = Bx . b )

assume b in Bags (n + 1) ; :: thesis: Ax . b = Bx . b

then reconsider b9 = b as Element of Bags (n + 1) ;

reconsider p2 = x9 . (b9 . n) as Polynomial of n,R by POLYNOM1:def 11;

n < n + 1 by NAT_1:13;

then reconsider bn = b9 | n as Element of Bags n by Th3;

thus Ax . b = p2 . bn by A37

.= Bx . b by A38 ; :: thesis: verum

end;assume b in Bags (n + 1) ; :: thesis: Ax . b = Bx . b

then reconsider b9 = b as Element of Bags (n + 1) ;

reconsider p2 = x9 . (b9 . n) as Polynomial of n,R by POLYNOM1:def 11;

n < n + 1 by NAT_1:13;

then reconsider bn = b9 | n as Element of Bags n by Th3;

thus Ax . b = p2 . bn by A37

.= Bx . b by A38 ; :: thesis: verum