How to define sums of naturals in the context of set theory

I am studying Hrbacek and Jech’s Introduction To Set Theory (3rd Ed), and on Section 3.4 there is the following problem:

For each finite sequence of natural numbers $langle k_i: 0 leq i < n rangle$. Define $sum langle k_i: 0 leq i < n rangle$ so that:

• $sum langle rangle = 0;$
• $sum langle k_0 rangle = k_0;$
• $sum langle k_i: 0 leq i < n+1 rangle = sum langle k_i: 0 leq i < n rangle + k_n$, for $n geq 1.$

So a little bit of context here: this section deals with (set-theoretically defined) natural numbers and the Recursion Theorem. Three versions of the Recursion Theorem are given, but in my opinion the following is to be used in this problem (the Parametric version of the Recursion Theorem – PVRT):

Let $a: P rightarrow A$ and $g: P times A times mathbb{N}
> rightarrow A$ be functions. There exists a unique function $f: P
> times mathbb{N} rightarrow A$ such that:

• $f(p, 0) = a(p)$ for all $p in P$;
• $f(p, n+1) = g(p, f(p,n), n)$ for all $n in mathbb{N}$ and all $p in P$.

I would appreciate any clue to finish the solution; if my approach is wrong, any pointer in the right direction would be appreciated. My attempt at a solution is this (notice $operatorname{Seq}{(S)}$ is the set of all finite sequences of elements in the set $S$):

Solution:

In PVRT we take $P = operatorname{Seq}{(mathbb{N})}$, $A = mathbb{N}$, and define $a: operatorname{Seq}{(mathbb{N})} rightarrow mathbb{N}$ as $a(k) = 0$ and $g: operatorname{Seq}{(mathbb{N})} times mathbb{N} times mathbb{N} rightarrow mathbb{N}$ as:

$$g(k, x, l) = begin{cases}
x + k_l, & text{if } l in operatorname{dom}{k}; \
x, & text{if } l notin operatorname{dom}{k}
end{cases}$$

By PVRT, there is a function $f: operatorname{Seq}{(mathbb{N})} times mathbb{N} rightarrow mathbb{N}$ such that:

• $f(k, 0) = a(k) = 0,$ for every $k in operatorname{Seq}{(mathbb{N})}$;
• $f(k, n+1) = g(k, f(k,n), n)$, for every $k in operatorname{Seq}{(mathbb{N})}$ and every $n in mathbb{N}$.

If $k in operatorname{Seq}{(mathbb{N})}$ y $operatorname{dom}{k} = l + 1 > 0$, notice that $f(k, l+1) = g(k, f(k, l), l) = f(k, l) + k_l$ (since $l < l+1$).

Now define $sum: operatorname{Seq}{(mathbb{N})} rightarrow mathbb{N}$ as $sum(k) = sum langle k_i: 0 leq i < operatorname{dom}{k} rangle = f(k, operatorname{dom}{k}).$

From this definition it is easy to see that:

1. $sum langle rangle = f(k, 0) = 0;$
2. $sum langle k_0 rangle = f(k, 1) = f(k, 0) + k_0 = k_0;$
3. $sum langle k_i: 0 leq i < n+1 rangle = f(k, n+1) = f(k, n) + k_n,$ for $n+1 > 1$.

My problem is with $3.$ It is intuitively clear for me, by the way $g$ (and hence $f$) was defined, that $f(k, n) = f(k[n], n)$, where $k[n]$ is the restriction of $k$ to the set $n$. However, I am having an incredibly difficult time proving this. I tried to prove this via induction:

• $forall n in mathbb{N}, forall k in operatorname{Seq}{(mathbb{N})},$ if $operatorname{dom}{k} = n+1$ then $f(k, n) = f(k[n], n)$.

I got stuck at one point, where I could no longer use the induction hypothesis. Then I tried to prove something stronger, hoping a stronger hypothesis would help:

• $forall n in mathbb{N}, forall m in mathbb{N}, forall k in operatorname{Seq}{(mathbb{N})},$ if $operatorname{dom}{k} = n$ and $m < n$ then $f(k, m) = f(k[m], m)$.

This time I got entangled in a dobule induction argument, where again the induction hypothesis was useless.

---

For the sake of completeness, I present the other two versions of the Recursion Theorem that appear in the book:

For any set $A$, any $a in A$ and any function $g: A times
> mathbb{N} rightarrow mathbb{N}$, there exists a unique infinite
sequence $f: mathbb{N} rightarrow A$ such that:

• $f_0 = a;$
• $f_{n+1} = g(f_n, n)$, for all $n in mathbb{N}$.

For any set $S$ and any function $g: operatorname{Seq}{(S)}
> rightarrow S$, there exists a unique sequence $f: mathbb{N}
> rightarrow S$ such that:

• $f_n = g(f[n])$, for all $n in mathbb{N}$.

---

I also noticed this question was asked recently here. However, since no solution was presented, I think it is pointless to comment there with a partial (and potentially incorrect) solution.