∀ {R : Type u_1} {S : Type u_4} [inst : Semiring R] [inst_1 : Monoid S] {M : Type u_6} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N₂ : Type u_9} [inst_5 : TopologicalSpace N₂]
  [inst_6 : AddCommMonoid N₂] [inst_7 : Module R N₂] {N₃ : Type u_10} [inst_8 : TopologicalSpace N₃]
  [inst_9 : AddCommMonoid N₃] [inst_10 : Module R N₃] [inst_11 : DistribMulAction S N₃] [inst_12 : SMulCommClass R S N₃]
  [inst_13 : ContinuousConstSMul S N₃] [inst_14 : DistribMulAction S N₂] [inst_15 : ContinuousConstSMul S N₂]
  [inst_16 : SMulCommClass R S N₂] [LinearMap.CompatibleSMul N₂ N₃ S R] (hₗ : N₂ →L[R] N₃) (c : S) (fₗ : M →L[R] N₂),
  hₗ.comp (c • fₗ) = c • hₗ.comp fₗ