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;

now :: thesis: for b9 being object st b9 in Bags (n + 1) holds
upmmpup . 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;

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