let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; 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; 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)); (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;
hence
(upm (n,R)) . ((mpu (n,R)) . p) = p
by FUNCT_2:12; verum