∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {R : Type u_3} {M : Type u_5}
  [inst_2 : TopologicalSpace M] [inst_3 : VAdd R M] [inst_4 : ContinuousConstVAdd R M] (r : R) (f : C(β, M))
  (g : C(α, β)), (r +ᵥ f).comp g = r +ᵥ f.comp g