a proof concerning fundamental group and lifting of paths

Question

Well, I put the theorem $54.3$ only to show that $\phi$ is well defined. I'm not sure why $\phi([f])= e_1 $ only by definition. Because to check that, I have first to lift $f$ and then compute $ \widetilde f(1) $

Answer 1

Yes, exactly, but its lift is the given path $\tilde f:e_0\leadsto e_1$ (because $f=p\circ\tilde f$) and its endpoint is $e_1$.

Answer 2

What's happened here is the proof is going backwards -- we are starting with the lift $\tilde{f}$. Since $f$ is defined to be $p \circ \tilde{f}$, then of course $\tilde{f}$ is a lift of $f$. By construction, $\tilde{f}(1) = e_1$, so $$\phi([f]) = \tilde{f}(1) = e_1.$$ Since Theorem 54.3 shows that $\phi$ is well-defined, i.e. we can choose any lift of $f$ to calculate $\phi([f])$, we see that everything is ok.