(𝕜 : Type u_1) →
  (E : Type u_4) →
    (Fₗ : Type u_6) →
      [inst : SeminormedAddCommGroup E] →
        [inst_1 : SeminormedAddCommGroup Fₗ] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : NormedSpace 𝕜 E] →
              [inst_4 : NormedSpace 𝕜 Fₗ] →
                (𝕜' : Type u_9) →
                  [inst_5 : NontriviallyNormedField 𝕜'] →
                    [inst_6 : NormedAlgebra 𝕜' 𝕜] →
                      [inst_7 : NormedSpace 𝕜' E] →
                        [IsScalarTower 𝕜' 𝕜 E] →
                          [inst_9 : NormedSpace 𝕜' Fₗ] →
                            [IsScalarTower 𝕜' 𝕜 Fₗ] →
                              (𝕜'' : Type u_10) →
                                [inst_11 : Ring 𝕜''] →
                                  [inst_12 : Module 𝕜'' Fₗ] →
                                    [inst_13 : ContinuousConstSMul 𝕜'' Fₗ] →
                                      [inst_14 : SMulCommClass 𝕜 𝕜'' Fₗ] →
                                        [inst_15 : SMulCommClass 𝕜' 𝕜'' Fₗ] → (E →L[𝕜] Fₗ) →ₗᵢ[𝕜''] E →L[𝕜'] Fₗ