Description: The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017)