∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℂ F] (m : E),
  LineDeriv.lineDerivOpCLM ℂ (TemperedDistribution E F) m =
    PointwiseConvergenceCLM.precomp F (-LineDeriv.lineDerivOpCLM ℂ (SchwartzMap E ℂ) m)