set P = upm (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

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

now :: thesis: for bn9 being object st bn9 in NAT holds
x . 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;

now :: thesis: for b9 being object st b9 in Bags n holds
xbn . 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;

hence x . bn9 = y . bn9 by FUNCT_2:12; :: thesis: verum

end;

hence x9 = y9 by FUNCT_2:12; :: thesis: verum

end;

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