∀ {𝕜 : Type u_3} [hnorm : NontriviallyNormedField 𝕜] {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F' : Type u_2}
  [inst_5 : AddCommGroup F'] [inst_6 : Module 𝕜 F'] [inst_7 : TopologicalSpace F'] [IsTopologicalAddGroup F']
  [ContinuousSMul 𝕜 F'] [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] (x x_1 : E →ₗ[𝕜] F'),
  Continuous ⇑(x + x_1)