Corollary 4

Let B and $B'$ be topological spaces, let $(E, p)$ be a locally trivial fibre space over B, let $f$ be a continuous mapping of $B'$ into B, let $\sigma : B'\times \mathbf{I}\rightarrow B$ be a homotopy starting from $f$, and let $\widetilde{f}$ be a continuous lifting of $f$ to E. If the space $B'$ is paracompact, there exists a homotopy $\widetilde{\sigma}: B'\times \mathbf{I}\rightarrow E$ starting from $\widetilde{f}$ which is a lifting of $\sigma$ to E.

Let $(E', p')$ be the $B'\times \mathbf{I}$-space deduced from $(E, p)$ by base change by the mapping $\sigma : B'\times \mathbf{I}\rightarrow B$. It is a locally trivial fibre space (I, p. 71, Corollary 2), and the mapping $s: B'\times \{0\} \rightarrow E'$ defined by $s((a,0)) = ((a,0),\widetilde{f}(a))$ for $a\in B'$ is a continuous section of $p'$ over $B'\times \{0\}$. By Proposition 2, there exists a continuous section $\widetilde{s}$ of $p'$ extending $s$. The mapping $\widetilde{\sigma}=$ pr$_2\circ \widetilde{s}$ has the required property.