for R being non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for n being Nat ex P being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) st P is RingIsomorphism