set PRPNR = Polynom-Ring (Polynom-Ring n,R);
set PN1R = Polynom-Ring (n + 1),R;
set PNR = Polynom-Ring n,R;
set CPN1R = the carrier of (Polynom-Ring (n + 1),R);
set P = upm n,R;
reconsider p1 = 1_ (Polynom-Ring (Polynom-Ring n,R)) as Polynomial of (Polynom-Ring n,R) by POLYNOM3:def 12;
reconsider p1' = 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 = p1' . x )
assume x in Bags (n + 1) ; :: thesis: p3 . x = p1' . 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;
A94: 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 A95: ( b | n = EmptyBag n & b . n = 0 ) ; :: thesis: p3 . b = p1' . b

then A96: b = (EmptyBag n) bag_extend 0 by Def1
.= EmptyBag (n + 1) by Th6 ;
p2 = (1_. (Polynom-Ring n,R)) . 0 by A95, POLYNOM3:def 12
.= 1_ (Polynom-Ring n,R) by POLYNOM3:31
.= 1_ n,R by POLYNOM1:90 ;
hence p3 . b = 1_ R by A94, A95, POLYNOM1:84
.= (1_ (n + 1),R) . b by A96, POLYNOM1:84
.= p1' . b by POLYNOM1:90 ;
:: thesis: verum

end;

suppose A97: ( b | n <> EmptyBag n or b . n <> 0 ) ; :: thesis: p3 . b = p1' . b

then b <> (EmptyBag n) bag_extend 0 by Def1;
then A98: b <> EmptyBag (n + 1) by Th6;

now

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

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

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

then p2 = 1_ (Polynom-Ring n,R) by A99, POLYNOM3:31
.= 1_ n,R by POLYNOM1:90 ;
hence p3 . b = 0. R by A94, A97, A100, A101, POLYNOM1:84; :: thesis: verum

end;

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

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

end;

end;

end;

hence p3 . b = (1_ (n + 1),R) . b by A98, POLYNOM1:84
.= p1' . b by POLYNOM1:90 ;
:: thesis: verum

end;

end;

end;

hence p3 . x = p1' . x ; :: thesis: verum

end;

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