Definition_by_Cases_is_Primitive_Recursive

Let $\mathcal R_1, \mathcal R_2, \ldots, \mathcal R_k$ be primitive recursive relations on $\N^l$ such that $\forall i, j \in \set{1, 2, \ldots, k}: \mathcal R_i \implies \lnot \mathcal R_j$, that is, all relations are mutually exclusive $\forall \tuple {n_1, n_2, \ldots, n_l} \in \N^l: \exists i \in \set {1, 2, \ldots, k}: \map {\mathcal R_i} {n_1, n_2, \ldots, n_l}$, that is, the set of relations is exhaustive. Let $\forall i \in \set {1, 2, \ldots, k}: g_i: \N^l \to \N$ be primitive recursive functions. Then the function $f: \N^l \to \N$ defined as $\map f {n_1, n_2, \ldots, n_l} = \begin{cases} \map {g_1} {n_1, n_2, \ldots, n_l} & : \map {\mathcal R_1} {n_1, n_2, \ldots, n_l} \\ \map {g_2} {n_1, n_2, \ldots, n_l} & : \map {\mathcal R_2} {n_1, n_2, \ldots, n_l} \\ \quad \vdots & \quad \vdots \\ \map {g_k} {n_1, n_2, \ldots, n_l} & : \map {\mathcal R_k} {n_1, n_2, \ldots, n_l} \end{cases}$ is primitive recursive.