∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i j : ι) (p : B × F), (p ∈ (Z.trivChange i j).source) = (p.1 ∈ Z.baseSet i ∩ Z.baseSet j)