∀ {E : Type u_5} {F : Type u_6} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E} {inst_2 : NormedAddCommGroup F}
  {inst_3 : NormedSpace ℝ F} {toFun : E → F} {smooth' : ContDiff ℝ (↑⊤) toFun}
  {decay' : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n toFun x‖ ≤ C} {toFun_1 : E → F}
  {smooth'_1 : ContDiff ℝ (↑⊤) toFun_1}
  {decay'_1 : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n toFun_1 x‖ ≤ C},
  { toFun := toFun, smooth' := smooth', decay' := decay' } =
      { toFun := toFun_1, smooth' := smooth'_1, decay' := decay'_1 } →
    toFun = toFun_1