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

now

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 12;
reconsider Py = (upm n,R) . y9 as Polynomial of (n + 1),R by POLYNOM1:def 27;
assume A121: (upm n,R) . x9 = (upm n,R) . y9 ; :: thesis: x9 = y9

now

let bn9 be set ; :: 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 27;

now

let b9 be set ; :: 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:18; :: thesis: verum

end;

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

end;

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