∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (K : Set X) (U : Set Z) (L : Set Y)
  (motive : (x : C(X, Y) × C(Y, Z)) → Set.MapsTo (⇑x.1) K (interior L) ∧ Set.MapsTo (⇑x.2) L U → Prop)
  (x : C(X, Y) × C(Y, Z)) (x_1 : Set.MapsTo (⇑x.1) K (interior L) ∧ Set.MapsTo (⇑x.2) L U),
  (∀ (f' : C(X, Y)) (g' : C(Y, Z)) (x : Set.MapsTo (⇑(f', g').1) K (interior L) ∧ Set.MapsTo (⇑(f', g').2) L U),
      motive (f', g') x) →
    motive x x_1