[proofplan]
We prove the identity directly from the definition of length as the supremum of metric variation sums over finite partitions of $[0,1]$. First, any partition of the concatenated path can be refined to include the joining time $1/2$, and the resulting sum splits into a variation sum for $\gamma$ plus a variation sum for $\eta$. This gives the upper bound. Conversely, near-optimal partitions for $\gamma$ and $\eta$ can be rescaled and joined into a partition of $\eta*\gamma$, giving the lower bound. Since both original lengths are finite, the equality also proves rectifiability of the concatenation.
[/proofplan]
[step:Define the variation sums used to compute path length]
Let $\alpha:[0,1]\to X$ denote the concatenated path $\alpha=\eta*\gamma$. Let $\mathcal{P}$ denote the set of finite partitions of $[0,1]$. For a path $\sigma:[0,1]\to X$, define the variation-sum map
\begin{align*}
V_\sigma:\mathcal{P}\to[0,\infty)
\end{align*}
by sending a partition
\begin{align*}
P=\{0=t_0<t_1<\cdots<t_m=1\}
\end{align*}
to
\begin{align*}
V_\sigma(P):=\sum_{i=1}^{m} d(\sigma(t_i),\sigma(t_{i-1})).
\end{align*}
Define the two-variable notation $V$ on pairs $(\sigma,P)$, where $\sigma:[0,1]\to X$ is a path and $P\in\mathcal{P}$, by
\begin{align*}
V(\sigma,P):=V_\sigma(P).
\end{align*}
By definition of path length,
\begin{align*}
L(\sigma)=\sup\{V(\sigma,P):P\text{ is a finite partition of }[0,1]\}.
\end{align*}
Since $\gamma$ and $\eta$ are rectifiable, $L(\gamma)<\infty$ and $L(\eta)<\infty$.
[/step]
[step:Bound every partition of the concatenation by the two component lengths]
Let
\begin{align*}
P=\{0=t_0<t_1<\cdots<t_m=1\}
\end{align*}
be a finite partition of $[0,1]$. If $1/2$ is not already a point of $P$, let $P'$ be the partition obtained by inserting $1/2$ into $P$; if $1/2\in P$, set $P'=P$. By the triangle inequality in $(X,d)$, inserting a point into a partition cannot decrease the variation sum, so
\begin{align*}
V(\alpha,P)\leq V(\alpha,P').
\end{align*}
Write the points of $P'$ lying in $[0,1/2]$ as
\begin{align*}
0=a_0<a_1<\cdots<a_r=\frac{1}{2}
\end{align*}
and the points of $P'$ lying in $[1/2,1]$ as
\begin{align*}
\frac{1}{2}=b_0<b_1<\cdots<b_s=1.
\end{align*}
Define partitions $A$ and $B$ of $[0,1]$ by
\begin{align*}
A:=\{2a_0,2a_1,\dots,2a_r\}
\end{align*}
and
\begin{align*}
B:=\{2b_0-1,2b_1-1,\dots,2b_s-1\}.
\end{align*}
Using the definition of $\alpha$ on the two subintervals gives
\begin{align*}
V(\alpha,P')=V(\gamma,A)+V(\eta,B).
\end{align*}
Since $A$ and $B$ are finite partitions of $[0,1]$, the definition of length gives
\begin{align*}
V(\gamma,A)\leq L(\gamma)
\end{align*}
and
\begin{align*}
V(\eta,B)\leq L(\eta).
\end{align*}
Therefore
\begin{align*}
V(\alpha,P)\leq L(\gamma)+L(\eta).
\end{align*}
Taking the supremum over all finite partitions $P$ of $[0,1]$ yields
\begin{align*}
L(\alpha)\leq L(\gamma)+L(\eta).
\end{align*}
[guided]
The goal of this step is to show that no partition of the concatenated path can collect more length than the length already present in the two pieces. Let
\begin{align*}
P=\{0=t_0<t_1<\cdots<t_m=1\}
\end{align*}
be a finite partition of $[0,1]$. The only point where the formula for $\alpha=\eta*\gamma$ changes is $1/2$, so we first make sure the partition sees that point. If $1/2$ is not a point of $P$, define $P'$ by inserting $1/2$ into $P$; if $1/2\in P$, define $P'=P$.
Why is this refinement allowed? Suppose a point $r$ is inserted between two consecutive partition points $a<r<b$. The triangle inequality gives
\begin{align*}
d(\alpha(b),\alpha(a))\leq d(\alpha(r),\alpha(a))+d(\alpha(b),\alpha(r)).
\end{align*}
All other terms in the variation sum are unchanged, so inserting $r$ cannot decrease the variation sum. Applying this to the insertion of $1/2$ gives
\begin{align*}
V(\alpha,P)\leq V(\alpha,P').
\end{align*}
Now list the points of $P'$ on the first half of the interval as
\begin{align*}
0=a_0<a_1<\cdots<a_r=\frac{1}{2}
\end{align*}
and the points of $P'$ on the second half as
\begin{align*}
\frac{1}{2}=b_0<b_1<\cdots<b_s=1.
\end{align*}
The first half of $\alpha$ is the path $\gamma$ traversed at twice the speed, so we rescale the first-half partition by defining
\begin{align*}
A:=\{2a_0,2a_1,\dots,2a_r\}.
\end{align*}
This is a finite partition of $[0,1]$ because $2a_0=0$, $2a_r=1$, and the order is preserved by multiplication by $2$. Similarly, the second half of $\alpha$ is the path $\eta$ traversed after the affine change of variables $u=2t-1$, so we define
\begin{align*}
B:=\{2b_0-1,2b_1-1,\dots,2b_s-1\}.
\end{align*}
This is also a finite partition of $[0,1]$.
Using the definition of the concatenation on each half, the variation sum along $P'$ splits exactly:
\begin{align*}
V(\alpha,P')=V(\gamma,A)+V(\eta,B).
\end{align*}
The equality includes the joining point because $\gamma(1)=y=\eta(0)$, so the endpoint of the first piece and the starting point of the second piece agree. Since $A$ is a partition of $[0,1]$, its variation sum for $\gamma$ is bounded above by the supremum defining $L(\gamma)$:
\begin{align*}
V(\gamma,A)\leq L(\gamma).
\end{align*}
Likewise,
\begin{align*}
V(\eta,B)\leq L(\eta).
\end{align*}
Combining these inequalities gives
\begin{align*}
V(\alpha,P)\leq V(\alpha,P')=V(\gamma,A)+V(\eta,B)\leq L(\gamma)+L(\eta).
\end{align*}
Because $P$ was arbitrary, taking the supremum over all finite partitions $P$ of $[0,1]$ proves
\begin{align*}
L(\alpha)\leq L(\gamma)+L(\eta).
\end{align*}
[/guided]
[/step]
[step:Build partitions of the concatenation from partitions of the two pieces]
Let $\varepsilon>0$. Since $L(\gamma)$ is the supremum of the variation sums of $\gamma$, there exists a finite partition
\begin{align*}
A=\{0=a_0<a_1<\cdots<a_r=1\}
\end{align*}
of $[0,1]$ such that
\begin{align*}
V(\gamma,A)>L(\gamma)-\frac{\varepsilon}{2}.
\end{align*}
Similarly, there exists a finite partition
\begin{align*}
B=\{0=b_0<b_1<\cdots<b_s=1\}
\end{align*}
of $[0,1]$ such that
\begin{align*}
V(\eta,B)>L(\eta)-\frac{\varepsilon}{2}.
\end{align*}
Define a finite partition $P$ of $[0,1]$ by
\begin{align*}
P:=\left\{\frac{a_0}{2},\frac{a_1}{2},\dots,\frac{a_r}{2},\frac{1+b_1}{2},\frac{1+b_2}{2},\dots,\frac{1+b_s}{2}\right\}.
\end{align*}
The point $(1+b_0)/2=1/2$ is already equal to $a_r/2$, so it is not listed twice.
By the definition of $\alpha$ on $[0,1/2]$ and $[1/2,1]$,
\begin{align*}
V(\alpha,P)=V(\gamma,A)+V(\eta,B).
\end{align*}
Hence
\begin{align*}
L(\alpha)\geq V(\alpha,P)>L(\gamma)+L(\eta)-\varepsilon.
\end{align*}
Since $\varepsilon>0$ was arbitrary,
\begin{align*}
L(\alpha)\geq L(\gamma)+L(\eta).
\end{align*}
[/step]
[step:Conclude equality and rectifiability]
The two inequalities prove
\begin{align*}
L(\alpha)=L(\gamma)+L(\eta).
\end{align*}
Because $\gamma$ and $\eta$ are rectifiable, both $L(\gamma)$ and $L(\eta)$ are finite. Therefore
\begin{align*}
L(\eta*\gamma)=L(\alpha)<\infty,
\end{align*}
so $\eta*\gamma$ is rectifiable. This proves the stated length formula.
[/step]
