∀ {ι : Type u_5} {B : Type u_6} [inst : TopologicalSpace B] {F : Type u_7} [inst_1 : TopologicalSpace F]
  (self : FiberBundleCore ι B F) (i j k : ι),
  ∀ x ∈ self.baseSet i ∩ self.baseSet j ∩ self.baseSet k,
    ∀ (v : F), self.coordChange j k x (self.coordChange i j x v) = self.coordChange i k x v