extended notion of unique homomorphisms, changed hom_map to the_uniq_map, started proof of fst_hom