set P = upm (n,R);

set PNR = Polynom-Ring (n,R);

thus upm (n,R) is additive :: thesis: verum

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;

.= ((upm (n,R)) . x) + ((upm (n,R)) . y) by POLYNOM1:def 11 ;

:: thesis: verum

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

hence (upm (n,R)) . (x + y) =
Px + Py
by FUNCT_2:12
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;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

.= ((upm (n,R)) . x) + ((upm (n,R)) . y) by POLYNOM1:def 11 ;

:: thesis: verum