Homotopy between loop and composite with constant loop

Statement

Existential version

Suppose $x_{0}$ is a point in a topological space $X$ and $f$ is a loop based at $x_{0}$, i.e., $f$ is a continuous map from $[0,1]$ to $X$ such that $f(0)=f(1)=x_{0}$. Suppose $e$ is the constant loop based at $x_{0}$, i.e., the loop that stays at $x_{0}$ throughout.

Denote by $*$ the composition of loops by concatenation. Then, $f$ is homotopic to the loops $e*f$ and $f*e$.

This statement is essentially the identity element part of the proof that the Fundamental group (?) of a based topological space is indeed a group.

Constructive/explicit version

For a loop $f$ based at $x_{0}$, the loop $e*f$ is given by:

$\!(e*f)(t)=\lbrace {\begin{array}{rl}x_{0},&0\leq t\leq 1/2\\f(2t-1),&1/2<t\leq 1\\\end{array}}$

The homotopy between $f$ and $e*f$ is given by:

$\!F_{\ell }(t,s)=\lbrace {\begin{array}{rl}x_{0},&0\leq t\leq s/2\\f((2t-s)/(2-s)),&s/2<t\leq 1\\\end{array}}$

The loop $f*e$ is given by:

$\!(f*e)(t)=\lbrace {\begin{array}{rl}f(2t),&0\leq t\leq 1/2\\x_{0},&1/2<t\leq 1\\\end{array}}$

The homotopy between $f$ and $f*e$ is given by:

Failed to parse (unknown function "\begin{array}"): {\displaystyle \! F_r(t,s) = \lbrace\begin{array}{rl} f(2t/(2 - s)), & 0 \le t \le (2 - s)/2 \\ x_0 , & (2 - s)/2 < t \le 1 }

Graphical version

Here is a pictorial description of the homotopy between $f$ and $e*f$:

Here is a pictorial description of the homotopy between $f$ and $f*e$: