∀ {B : Type u_2} (F : Type u_3) {X : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace B]
  [inst_2 : TopologicalSpace F] {E : B → Type u_5} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (b : B) → TopologicalSpace (E b)] [inst_5 : FiberBundle F E] (f : X → Bundle.TotalSpace F E) {s : Set X}
  {x₀ : X},
  ContinuousWithinAt f s x₀ ↔
    ContinuousWithinAt (fun x => (f x).proj) s x₀ ∧
      ContinuousWithinAt (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀