∀ {ι : Type u_1} {R : Type u_3} [inst : Semiring R] {β : ι → Type u_7} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9}
  [inst_1 : (i : ι) → AddCommMonoid (β i)] [inst_2 : (i : ι) → AddCommMonoid (β₁ i)]
  [inst_3 : (i : ι) → AddCommMonoid (β₂ i)] [inst_4 : (i : ι) → Module R (β i)] [inst_5 : (i : ι) → Module R (β₁ i)]
  [inst_6 : (i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) (f₂ : (i : ι) → β i →ₗ[R] β₁ i),
  (DFinsupp.mapRange.linearMap fun i => f i ∘ₗ f₂ i) = DFinsupp.mapRange.linearMap f ∘ₗ DFinsupp.mapRange.linearMap f₂