Let $F:C\to Set$ be a functor. Let $\int F$ be the category of elements. Let $\prod:\int F\to C$ be the canonical forgetful functor. Then for any morphism $f:c\to d$ and any object $(c,x)$ in the fiber of $c$, there is a unique lift of the morphism $f$ to a morphism in $\int F$ with domain $(c,x)$ that projects along $\prod$ to $f$.
My question is how do I prove the existence of a lift? Would I construct it or define it? If so, how do I do it?