∀ {X : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : MulAction G X] {g f : X → X} {B A : Set X} {T S : Finset G},
  Equidecomp.IsDecompOn g B T → Equidecomp.IsDecompOn f A S → Set.MapsTo f A B → Equidecomp.IsDecompOn (g ∘ f) A (T * S)