∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {g : E →ₗ[𝕜] F}
  (hg :
    ∀ (u : ℕ → E) (x : E) (y : F),
      Filter.Tendsto u Filter.atTop (nhds x) → Filter.Tendsto (⇑g ∘ u) Filter.atTop (nhds y) → y = g x),
  ⇑(ContinuousLinearMap.ofSeqClosedGraph hg) = ⇑g