∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  {G : CategoryTheory.Subfunctor F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)},
  G.IsGeneratedBy x →
    ∀ {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ F'), (G.image f).IsGeneratedBy fun i => f.app (X i) (x i)