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

now

let x', y' be Element of (Polynom-Ring (Polynom-Ring n,R)); :: thesis: ( (upm n,R) . x' = (upm n,R) . y' implies x' = y' )
reconsider x = x', y = y' as Polynomial of (Polynom-Ring n,R) by POLYNOM3:def 12;
reconsider Py = (upm n,R) . y' as Polynomial of (n + 1),R by POLYNOM1:def 27;
assume A121: (upm n,R) . x' = (upm n,R) . y' ; :: thesis: x' = y'

now

let bn' be set ; :: thesis: ( bn' in NAT implies x . bn' = y . bn' )
assume bn' in NAT ; :: thesis: x . bn' = y . bn'
then reconsider bn = bn' as Element of NAT ;
reconsider xbn = x . bn, ybn = y . bn as Polynomial of n,R by POLYNOM1:def 27;

now

let b' be set ; :: thesis: ( b' in Bags n implies xbn . b' = ybn . b' )
assume b' in Bags n ; :: thesis: xbn . b' = ybn . b'
then reconsider b = b' as bag of by PRE_POLY:def 12;
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 . b' = ybn . b' ; :: thesis: verum

end;

hence x . bn' = y . bn' by FUNCT_2:18; :: thesis: verum

end;

hence x' = y' by FUNCT_2:18; :: thesis: verum

end;

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