∀ {X : TopCat} (F : TopCat.Sheaf CommRingCat X) {U V W UW VW : TopologicalSpace.Opens ↑X} (e : W ≤ U ⊔ V)
  (x :
    ↑{
        carrier :=
          ↥(((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp
                  (RingHom.fst ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))).eqLocus
              ((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp
                (RingHom.snd ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V))))),
        commRing :=
          (((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp
                  (RingHom.fst ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V)))).eqLocus
              ((CommRingCat.Hom.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)).comp
                (RingHom.snd ↑(F.val.obj (Opposite.op U)) ↑(F.val.obj (Opposite.op V))))).toCommRing })
  (y : ↑(F.val.obj (Opposite.op W))) (h₁ : UW = U ⊓ W) (h₂ : VW = V ⊓ W),
  (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE e).op))
        ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) =
      y ↔
    (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) (↑x).1 =
        (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) y ∧
      (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) (↑x).2 =
        (CategoryTheory.ConcreteCategory.hom (F.val.map (CategoryTheory.homOfLE ⋯).op)) y