Real Power of a Positive Real Number

Let $\mathbb{R}$ be the real numbers, let $\exp$ be the exponential function and let $\log:(0,\infty)\to\mathbb{R}$ be the natural logarithm. For a real number $t>0$ and a real number $a$, the real power of $t$ with exponent $a$ is

$$t^{a}=\exp\bigl(a\log t\bigr).$$