set P = upm n,R;
set PNR = Polynom-Ring n,R;
thus upm n,R is additive :: thesis: verum

proof

let x, y be Element of (Polynom-Ring (Polynom-Ring n,R)); :: according to GRCAT_1:def 13 :: thesis: (upm n,R) . (x + y) = ((upm n,R) . x) + ((upm n,R) . y)
reconsider x9 = x, y9 = y, xy9 = x + y as Polynomial of (Polynom-Ring n,R) by POLYNOM3:def 12;
reconsider Pxy = (upm n,R) . (x + y), Px = (upm n,R) . x, Py = (upm n,R) . y as Polynomial of (n + 1),R by POLYNOM1:def 27;
A1: xy9 = x9 + y9 by POLYNOM3:def 12;

now

let b be set ; :: thesis: ( b in Bags (n + 1) implies Pxy . b = (Px + Py) . b )
assume b in Bags (n + 1) ; :: thesis: Pxy . b = (Px + Py) . b
then reconsider b9 = b as bag of n + 1 by PRE_POLY:def 12;
reconsider xybn = (x9 + y9) . (b9 . n) as Polynomial of n,R by POLYNOM1:def 27;
reconsider xbn = x9 . (b9 . n), ybn = y9 . (b9 . n) as Polynomial of n,R by POLYNOM1:def 27;
n < n + 1 by XREAL_1:31;
then reconsider bn = b9 | n as bag of n by Th3;
A2: ( xbn . bn = Px . b9 & ybn . bn = Py . b9 ) by Def6;
(x9 + y9) . (b9 . n) = (x9 . (b9 . n)) + (y9 . (b9 . n)) by NORMSP_1:def 5;
then xybn = xbn + ybn by POLYNOM1:def 27;
hence Pxy . b = (xbn + ybn) . bn by A1, Def6
.= (Px . b9) + (Py . b9) by A2, POLYNOM1:def 21
.= (Px + Py) . b by POLYNOM1:def 21 ;
:: thesis: verum

end;

hence (upm n,R) . (x + y) = Px + Py by FUNCT_2:18
.= ((upm n,R) . x) + ((upm n,R) . y) by POLYNOM1:def 27 ;
:: thesis: verum

end;