let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis: for n being Nat

for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p

let n be Nat; :: thesis: for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p

let p be Element of (Polynom-Ring ((n + 1),R)); :: thesis: (upm (n,R)) . ((mpu (n,R)) . p) = p

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

reconsider p9 = p as Polynomial of (n + 1),R by POLYNOM1:def 11;

reconsider upmmpup = (upm (n,R)) . ((mpu (n,R)) . p) as Polynomial of (n + 1),R by POLYNOM1:def 11;

reconsider mpup = (mpu (n,R)) . p as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def 10;

for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p

let n be Nat; :: thesis: for p being Element of (Polynom-Ring ((n + 1),R)) holds (upm (n,R)) . ((mpu (n,R)) . p) = p

let p be Element of (Polynom-Ring ((n + 1),R)); :: thesis: (upm (n,R)) . ((mpu (n,R)) . p) = p

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

reconsider p9 = p as Polynomial of (n + 1),R by POLYNOM1:def 11;

reconsider upmmpup = (upm (n,R)) . ((mpu (n,R)) . p) as Polynomial of (n + 1),R by POLYNOM1:def 11;

reconsider mpup = (mpu (n,R)) . p as Polynomial of (Polynom-Ring (n,R)) by POLYNOM3:def 10;

now :: thesis: for b9 being object st b9 in Bags (n + 1) holds

upmmpup . b9 = p9 . b9

hence
(upm (n,R)) . ((mpu (n,R)) . p) = p
by FUNCT_2:12; :: thesis: verumupmmpup . b9 = p9 . b9

let b9 be object ; :: thesis: ( b9 in Bags (n + 1) implies upmmpup . b9 = p9 . b9 )

assume b9 in Bags (n + 1) ; :: thesis: upmmpup . b9 = p9 . b9

then reconsider b = b9 as Element of Bags (n + 1) ;

reconsider mpupbn = mpup . (b . n) as Polynomial of n,R by POLYNOM1:def 11;

n < n + 1 by NAT_1:13;

then reconsider bn = b | n as bag of n by Th3;

A1: b = bn bag_extend (b . n) by Def1;

thus upmmpup . b9 = mpupbn . bn by Def6

.= p9 . b9 by A1, Def7 ; :: thesis: verum

end;assume b9 in Bags (n + 1) ; :: thesis: upmmpup . b9 = p9 . b9

then reconsider b = b9 as Element of Bags (n + 1) ;

reconsider mpupbn = mpup . (b . n) as Polynomial of n,R by POLYNOM1:def 11;

n < n + 1 by NAT_1:13;

then reconsider bn = b | n as bag of n by Th3;

A1: b = bn bag_extend (b . n) by Def1;

thus upmmpup . b9 = mpupbn . bn by Def6

.= p9 . b9 by A1, Def7 ; :: thesis: verum