Let $X$ be a D11: Set such that

(i)	$f : X \to [0, \infty]$ is an D4361: Unsigned basic function on $X$

Let $p \in (0, \infty)$ be a D993: Real number.

Then \begin{equation} f(x)^p = \int^{\infty}_0 I_{\{ f(x) > t \}}(x) p t^{p - 1} \, d t \end{equation}

Let $X$ be a D11: Set such that

(i)	$f : X \to [0, \infty]$ is an D4361: Unsigned basic function on $X$

Let $p \in (0, \infty)$ be a D993: Real number.

Then \begin{equation} f(x)^p = \int^{\infty}_0 I_{\{ f(x) > t \}}(x) \, d t^p \end{equation}