(*#*
This definition yields a well defined, strongly extensional function
which extends the algebraic exponentiation to an integer power and
(*#*
This definition yields a well defined, strongly extensional function
which extends the algebraic exponentiation to an integer power and