A more rigorous proof on a Bellman-Ford's corollary
I think your proof is correct, but there are 2 things that I would like to comment:

I think that when you are proving the $\rightarrow$ direction and you say:


&quot;Each edge of the path $p$ will be relaxed by Bellman-Ford, an operation which will only decrease $v.d$. Therefore we can conclude, that $v.d &lt; \infty$
after the algorithm terminates.&quot;

there is an assumption that a call to RELAX will necessarily decrease $v.d$. But this is not necessarily true, as a call to RELAX can leave $v.d$ untouched. So, you would need to prove that in BELLMAN-FORD there would be a call to RELAX that necessarily decreases $v.d$.
The alternative argument you are proposing (use the &quot;Path-relaxation property&quot;) would work fine here, though.

Since this is a corollary, I think the authors expected you to use the previous Lemma to solve it (of course, solving it via a different reasoning is ok too).
In this case, we have Lemma 24.2:


Lemma 24.2
Let $G = (V, E)$ be a weighted, directed graph with source $s$ and weight function $w: E \rightarrow \mathbb{R}$, and assume that $G$ contains no negative-weight cycles that are reachable from $s$. Then, after the $|V| - 1$ iterations of the for loop of lines 2-4 of BELLMAN-FORD, we have $v.d = \delta(s, v)$ for all vertices that are reachable from $s$.

We can use it to prove the corollary:
$\rightarrow$: If there is a path from $s$ to $v$, by Lemma 24.2, we have $v.d = \delta(s, v)$, where $\delta(s, v)$ (the shortest path weight from $s$ to $v$) is less than $\infty$ since there is a path.
$\leftarrow$: If BELLMAN-FORD terminates with $v.d &lt; \infty$ when it is run on $G$, by Lemma 24.2 we have that $\delta(s, v) = v.d &lt; \infty$, which by definition of $\delta$ means that there is a path from $s$ to $v$.