∀ {α : Type u_6} [inst : AddCommMonoid α] (m M N : ℕ) (f : (n : ℕ) × (Fin n → ℕ) → α) (g : (n : ℕ) × Composition n → α),
  (∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ FormalMultilinearSeries.compPartialSumSource m M N),
      f e = g (FormalMultilinearSeries.compChangeOfVariables m M N e he)) →
    ∑ e ∈ FormalMultilinearSeries.compPartialSumSource m M N, f e =
      ∑ e ∈ FormalMultilinearSeries.compPartialSumTarget m M N, g e