# a proof concerning fundamental group and lifting of paths

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

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