(𝕜 : Type u) →
  {n : ℕ} →
    (Ei : Fin n.succ → Type wEi) →
      (G : Type wG) →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  (p : Fin (n + 1)) →
                    ContinuousMultilinearMap 𝕜 Ei G ≃ₗᵢ[𝕜]
                      Ei p →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei (p.succAbove i)) G