Homotopy between composites of homotopic loops

Statement

Existential version

Suppose $X$ is a topological space, $x_0$ is a point in $X$, and $f_1,g_1,f_2,g_2$ are loops based at $x_0$ with the property that $f_1$ is homotopic to $g_1$ (as a loop based at $x_0$) and $f_2$ is homotopic to $g_2$ (again, as a loop based at $x_0$). Then, $f_1*f_2$ is homotopic to $g_1*g_2$.

Constructive/explicit version

More explicitly, suppose $F_1$ is a homotopy from $f_1$ to $g_1$. In other words, $F_1:S^1\times I\to X$ is a continuous map (where $S^1$ is the circle, viewed as $[0,1]$ with endpoints identified, and $I=[0,1]$ is the closed unit interval) having the following properties:

• $F_1(s,0)=f_1(s)$
• $F_1(s,1)=g_1(s)$
• $F_1(0,t)=x_0$ (here $0\sim 1$ is the chosen basepoint of the circle from which we're mapping). This says that the loop always remains based on $x_0$.

Similarly, suppose $F_2:S^1\times I\to X$ is a continuous map having the following properties:

• $F_2(s,0)=f_2(s)$
• $F_2(s,1)=g_2(s)$
• $F_2(0,t)=x_0$ (here $0\sim 1$ is the chosen basepoint of the circle). This says that the loop always remains based on $x_0$.

Then, we can consider the following homotopy from $f_1*f_2$ to $g_1*g_2$:

$F(s,t):=\{\begin{array}{cc}{F}_1(2s,t),& 0\le t\le 1/2\\ F_2(2s-1,t),& 1/2<t\le 1\\ \end{array}$

We can think of $F$ as $F_1*F_2$.