∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis)
  (σ τ : ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g)) (x : α),
  a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)