$thm:lexprod-hom$. A homomorphism $f : F → G ⋅ H$ induces the partition of $V(F)$ whose classes are the connected components of the subgraphs induced on the fibres of the first coordinate of $f$; it is the unique partition into connected parts with which $f$ is compatible, in the sense that it refines those fibres and that no edge inside a fibre crosses two of its classes. Splitting the hom-set along this partition and pairing the two coordinates of $f$ with a homomorphism out of the quotient and one out of the disjoint union of the classes gives the bijection.