set P = upm (n,R);
set PNR = Polynom-Ring (n,R);
set PN1R = Polynom-Ring ((n + 1),R);
set PRPNR = Polynom-Ring (Polynom-Ring (n,R));
set CPN1R = the carrier of (Polynom-Ring ((n + 1),R));
reconsider p1 = 1_ (Polynom-Ring (Polynom-Ring (n,R))) as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def 10;
reconsider p19 = 1_ (Polynom-Ring ((n + 1),R)) as Polynomial of (n + 1),R by POLYNOM1:def 11;
(upm (n,R)) . (1_ (Polynom-Ring (Polynom-Ring (n,R)))) in the carrier of (Polynom-Ring ((n + 1),R))
;
then reconsider p3 = (upm (n,R)) . p1 as Polynomial of (n + 1),R by POLYNOM1:def 11;
then
p19 = p3
;
hence
upm (n,R) is unity-preserving
by GROUP_1:def 13; verum