for R being non empty 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