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;

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

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

then
p19 = p3
;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;

end;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 . bend;

hence
p3 . x = p19 . x
; :: thesis: verumper cases
( ( b | n = EmptyBag n & b . n = 0 ) or b | n <> EmptyBag n or b . n <> 0 )
;

end;

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;.= 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

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

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;

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

b <> (EmptyBag n) bag_extend 0
by A116, Def1;
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;

end;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 )
;

end;

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;.= 1_ (n,R) by POLYNOM1:31 ;

hence p3 . b = 0. R by A113, A116, A118, A120, POLYNOM1:25; :: thesis: verum

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;.= 0_ (n,R) by POLYNOM1:def 11 ;

hence p3 . b = 0. R by A113, A118, POLYNOM1:22; :: thesis: verum

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

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