Rigorous definition of the kinship coefficient and proof of a recursion thereof

I am reading Section 5.2, Kinship and Inbreeding Coefficients, of Kenneth Lange, Mathematical and Statistical Methods for Genetic Analysis. There the kinship coefficient $Phi_{i,j}$ is defined for two relatives $i$ and $j$ as the probability that a gene selected randomly from $i$ and a gene selected randomly from the same autosomal locus of j are identical by descent. Then the book states that suppose $k$ and $l$ are the parents of $i$,
$$Phi_{i,j}=frac12(Phi_{k,j}+Phi_{l,j}) tag1$$
with some exceptions.

---

Equation (1) seems intuitive. Yet it is slippery for a proof especially considering the exceptions. The root cause is that the definition of $Phi_{i,j}$ is vague albeit seemingly plausible. I am seeking a mathematically rigorous definition of $Phi_{i,j}$ and a proof for Equation (1) together with the condition under which it applies.