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 VECTSP_1:def 19 :: 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 10;
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 11;
A1: xy9 = x9 + y9 by POLYNOM3:def 10;

now :: thesis: for b being object st b in Bags (n + 1) holds
Pxy . b = (Px + Py) . b

let b be object ; :: 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 ;
reconsider xybn = (x9 + y9) . (b9 . n) as Polynomial of n,R by POLYNOM1:def 11;
reconsider xbn = x9 . (b9 . n), ybn = y9 . (b9 . n) as Polynomial of n,R by POLYNOM1:def 11;
n < n + 1 by XREAL_1:29;
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 2;
then xybn = xbn + ybn by POLYNOM1:def 11;
hence Pxy . b = (xbn + ybn) . bn by A1, Def6
.= (Px . b9) + (Py . b9) by A2, POLYNOM1:15
.= (Px + Py) . b by POLYNOM1:15 ;
:: thesis: verum

end;

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

end;