set P = upm (n,R);

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

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

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

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

now :: thesis: for x9, y9 being Element of (Polynom-Ring (Polynom-Ring (n,R))) st (upm (n,R)) . x9 = (upm (n,R)) . y9 holds

x9 = y9

hence
upm (n,R) is one-to-one
by WAYBEL_1:def 1; :: thesis: verumx9 = y9

let x9, y9 be Element of (Polynom-Ring (Polynom-Ring (n,R))); :: thesis: ( (upm (n,R)) . x9 = (upm (n,R)) . y9 implies x9 = y9 )

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

reconsider Py = (upm (n,R)) . y9 as Polynomial of (n + 1),R by POLYNOM1:def 11;

assume A121: (upm (n,R)) . x9 = (upm (n,R)) . y9 ; :: thesis: x9 = y9

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

reconsider Py = (upm (n,R)) . y9 as Polynomial of (n + 1),R by POLYNOM1:def 11;

assume A121: (upm (n,R)) . x9 = (upm (n,R)) . y9 ; :: thesis: x9 = y9

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

x . bn9 = y . bn9

hence
x9 = y9
by FUNCT_2:12; :: thesis: verumx . bn9 = y . bn9

let bn9 be object ; :: thesis: ( bn9 in NAT implies x . bn9 = y . bn9 )

assume bn9 in NAT ; :: thesis: x . bn9 = y . bn9

then reconsider bn = bn9 as Element of NAT ;

reconsider xbn = x . bn, ybn = y . bn as Polynomial of n,R by POLYNOM1:def 11;

end;assume bn9 in NAT ; :: thesis: x . bn9 = y . bn9

then reconsider bn = bn9 as Element of NAT ;

reconsider xbn = x . bn, ybn = y . bn as Polynomial of n,R by POLYNOM1:def 11;

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

xbn . b9 = ybn . b9

hence
x . bn9 = y . bn9
by FUNCT_2:12; :: thesis: verumxbn . b9 = ybn . b9

let b9 be object ; :: thesis: ( b9 in Bags n implies xbn . b9 = ybn . b9 )

assume b9 in Bags n ; :: thesis: xbn . b9 = ybn . b9

then reconsider b = b9 as bag of n ;

set bn1 = b bag_extend bn;

A122: ( (b bag_extend bn) | n = b & (b bag_extend bn) . n = bn ) by Def1;

then xbn . b = Py . (b bag_extend bn) by A121, Def6

.= ybn . b by A122, Def6 ;

hence xbn . b9 = ybn . b9 ; :: thesis: verum

end;assume b9 in Bags n ; :: thesis: xbn . b9 = ybn . b9

then reconsider b = b9 as bag of n ;

set bn1 = b bag_extend bn;

A122: ( (b bag_extend bn) | n = b & (b bag_extend bn) . n = bn ) by Def1;

then xbn . b = Py . (b bag_extend bn) by A121, Def6

.= ybn . b by A122, Def6 ;

hence xbn . b9 = ybn . b9 ; :: thesis: verum