let R be non empty non trivial right_complementable Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: for n being Element of NAT
for p being Element of (Polynom-Ring (n + 1),R) holds (upm n,R) . ((mpu n,R) . p) = p
let n be Element of 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 27;
reconsider upmmpup = (upm n,R) . ((mpu n,R) . p) as Polynomial of (n + 1),R by POLYNOM1:def 27;
reconsider mpup = (mpu n,R) . p as Polynomial of (Polynom-Ring n,R) by POLYNOM3:def 12;

now

let b9 be set ; :: 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 27;
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:18; :: thesis: verum