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\left({\frac {2t-s}{2-s}}\right),&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:

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

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$: