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):=\lbrace {\begin{array}{rl}F_{1}(2s,t),&0\leq t\leq 1/2\\F_{2}(2s-1,t),&1/2<t\leq 1\\\end{array}}$

We can think of $F$ as $F_{1}*F_{2}$.