∀ {𝕜 : Type u_4} {E : Type u_1} {F : Type u_3} {F' : Type u_2} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedAddCommGroup F'] [inst_7 : NormedSpace ℝ F'] [inst_8 : NormedSpace 𝕜 F']
  {n : ℕ∞} {K : TopologicalSpace.Compacts E} [inst_9 : LinearMap.CompatibleSMul F F' ℝ 𝕜] (T : F →L[𝕜] F')
  (f g : ContDiffMapSupportedIn E F n K),
  { toFun := ⇑T ∘ ⇑(f + g), contDiff' := ⋯, zero_on_compl' := ⋯ } =
    { toFun := ⇑T ∘ ⇑f, contDiff' := ⋯, zero_on_compl' := ⋯ } +
      { toFun := ⇑T ∘ ⇑g, contDiff' := ⋯, zero_on_compl' := ⋯ }