∀ {𝕜 : Type u_8} {F₁ : Type u_9} {F₂ : Type u_10} {B₁ : Type u_11} {B₂ : Type u_12} {M : Type u_13}
  {E₁ : B₁ → Type u_14} {E₂ : B₂ → Type u_15} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (x : B₁) → AddCommGroup (E₁ x)] [inst_2 : (x : B₁) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁]
  [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B₁) → TopologicalSpace (E₁ x)] [inst_7 : (x : B₂) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B₂) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B₂) → TopologicalSpace (E₂ x)]
  [inst_13 : TopologicalSpace B₁] [inst_14 : TopologicalSpace B₂] [inst_15 : TopologicalSpace M]
  [inst_16 : FiberBundle F₁ E₁] [inst_17 : VectorBundle 𝕜 F₁ E₁] [inst_18 : FiberBundle F₂ E₂]
  [inst_19 : VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)}
  {v : (m : M) → E₁ (b₁ m)} {s : Set M},
  ContinuousWithinAt (fun m => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s m₀ →
    ContinuousWithinAt (fun m => { proj := b₁ m, snd := v m }) s m₀ →
      ContinuousWithinAt b₂ s m₀ → ContinuousWithinAt (fun m => { proj := b₂ m, snd := (ϕ m) (v m) }) s m₀