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 12;
reconsider p19 = 1_ (Polynom-Ring (n + 1),R) as Polynomial of (n + 1),R by POLYNOM1:def 27;
(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 27;

now

let x be set ; :: thesis: ( x in Bags (n + 1) implies p3 . x = p19 . x )
assume x in Bags (n + 1) ; :: thesis: p3 . x = p19 . x
then reconsider b = x as Element of Bags (n + 1) ;
reconsider p2 = p1 . (b . n) as Polynomial of n,R by POLYNOM1:def 27;
A113: p3 . b = p2 . (b | n) by Def6;

now

per cases ( ( b | n = EmptyBag n & b . n = 0 ) or b | n <> EmptyBag n or b . n <> 0 ) ;

suppose A114: ( b | n = EmptyBag n & b . n = 0 ) ; :: thesis: p3 . b = p19 . b

then A115: b = (EmptyBag n) bag_extend 0 by Def1
.= EmptyBag (n + 1) by Th6 ;
p2 = (1_. (Polynom-Ring n,R)) . 0 by A114, POLYNOM3:def 12
.= 1_ (Polynom-Ring n,R) by POLYNOM3:31
.= 1_ n,R by POLYNOM1:90 ;
hence p3 . b = 1_ R by A113, A114, POLYNOM1:84
.= (1_ (n + 1),R) . b by A115, POLYNOM1:84
.= p19 . b by POLYNOM1:90 ;
:: thesis: verum

end;

suppose A116: ( b | n <> EmptyBag n or b . n <> 0 ) ; :: thesis: p3 . b = p19 . b

A117: now

n < n + 1 by NAT_1:13;
then A118: b | n is bag of n by Th3;
A119: p2 = (1_. (Polynom-Ring n,R)) . (b . n) by POLYNOM3:def 12;

per cases ( b . n = 0 or b . n <> 0 ) ;

suppose A120: b . n = 0 ; :: thesis: p3 . b = 0. R

then p2 = 1_ (Polynom-Ring n,R) by A119, POLYNOM3:31
.= 1_ n,R by POLYNOM1:90 ;
hence p3 . b = 0. R by A113, A116, A118, A120, POLYNOM1:84; :: thesis: verum

end;

suppose b . n <> 0 ; :: thesis: p3 . b = 0. R

then p2 = 0. (Polynom-Ring n,R) by A119, POLYNOM3:31
.= 0_ n,R by POLYNOM1:def 27 ;
hence p3 . b = 0. R by A113, A118, POLYNOM1:81; :: thesis: verum

end;

end;

end;

b <> (EmptyBag n) bag_extend 0 by A116, Def1;
then b <> EmptyBag (n + 1) by Th6;
hence p3 . b = (1_ (n + 1),R) . b by A117, POLYNOM1:84
.= p19 . b by POLYNOM1:90 ;
:: thesis: verum

end;

end;

end;

hence p3 . x = p19 . x ; :: thesis: verum

end;

then p19 = p3 by FUNCT_2:18;
hence upm n,R is unity-preserving by GROUP_1:def 17; :: thesis: verum