∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q U : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) (f : P ⟶ Q) (g : Q ⟶ U),
  (x.map f).map g = x.map (CategoryTheory.CategoryStruct.comp f g)