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 x' = x, y' = y, xy' = 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: xy' = x' + y' 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 b' = b as bag of by PRE_POLY:def 12;
reconsider xybn = (x' + y') . (b' . n) as Polynomial of n,R by POLYNOM1:def 27;
reconsider xbn = x' . (b' . n), ybn = y' . (b' . n) as Polynomial of n,R by POLYNOM1:def 27;
n < n + 1 by XREAL_1:31;
then reconsider bn = b' | n as bag of by Th3;
A2: ( xbn . bn = Px . b' & ybn . bn = Py . b' ) by Def6;
(x' + y') . (b' . n) = (x' . (b' . n)) + (y' . (b' . n)) by NORMSP_1:def 5;
then xybn = xbn + ybn by POLYNOM1:def 27;
hence Pxy . b = (xbn + ybn) . bn by A1, Def6
.= (Px . b') + (Py . b') 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;