∀ {𝕜 : Type u_3} {𝕜₂ : Type u_4} {E : Type u_5} {Eₗ : Type u_2} {F : Type u_6} {Fₗ : Type u_1} [inst : NormedField 𝕜]
  [inst_1 : NormedField 𝕜₂] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] [inst_6 : NormedAddCommGroup Eₗ] [inst_7 : NormedSpace 𝕜 Eₗ] [inst_8 : CompleteSpace Eₗ]
  [inst_9 : NormedAddCommGroup Fₗ] [inst_10 : NormedSpace 𝕜₂ Fₗ] [inst_11 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_12 : RingHomInvPair σ₁₂ σ₂₁] [inst_13 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂)
  (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) (h_norm₂ : ∀ (x : F), ‖e₁ (f.symm x)‖ = ‖e₂ x‖) (x : Eₗ),
  ‖(f.extend e₁ e₂ h_dense₁ ⋯ h_dense₂ ⋯).toLinearEquiv x‖ = ‖x‖