The
standard real exponentiation function with
exponent $p \in \mathbb{R}$ is the
D4364: Real function
\begin{equation}
\begin{cases}
\mathbb{R} \setminus \{ 0 \} \to \mathbb{R}, \quad & x \mapsto x^p, \qquad \text{ if } p < 0 \\
\mathbb{R} \to \mathbb{R}, \quad & x \mapsto x^p, \qquad \text{ if } p \geq 0 \\
\end{cases}
\end{equation}
