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;

now :: thesis: for x being object st x in Bags (n + 1) holds
p3 . x = p19 . x

let x be object ; :: 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 11;
A113: p3 . b = p2 . (b | n) by Def6;

now :: thesis: p3 . b = p19 . b

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 10
.= 1_ (Polynom-Ring (n,R)) by POLYNOM3:30
.= 1_ (n,R) by POLYNOM1:31 ;
hence p3 . b = 1_ R by A113, A114, POLYNOM1:25
.= (1_ ((n + 1),R)) . b by A115, POLYNOM1:25
.= p19 . b by POLYNOM1:31 ;
:: thesis: verum

end;

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

A117: now :: thesis: p3 . b = 0. R

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 10;

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:30
.= 1_ (n,R) by POLYNOM1:31 ;
hence p3 . b = 0. R by A113, A116, A118, A120, POLYNOM1:25; :: thesis: verum

end;

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

then p2 = 0. (Polynom-Ring (n,R)) by A119, POLYNOM3:30
.= 0_ (n,R) by POLYNOM1:def 11 ;
hence p3 . b = 0. R by A113, A118, POLYNOM1:22; :: 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:25
.= p19 . b by POLYNOM1:31 ;
:: thesis: verum

end;

end;

end;

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

end;

then p19 = p3 ;
hence upm (n,R) is unity-preserving by GROUP_1:def 13; :: thesis: verum