∀ (E : Type u_1) (F : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : NormedSpace ℝ E] (f g : SchwartzMap E F) (x : E), fderiv ℝ (⇑f + ⇑g) x = fderiv ℝ (⇑f) x + fderiv ℝ (⇑g) x