∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : Group X] [IsTopologicalGroup X]
  [inst_3 : UniformSpace Y] [inst_4 : CommGroup Y] [IsUniformGroup Y] [T0Space Y] [CompactSpace Y]
  [LocallyCompactSpace X] (V : ℕ → Set Y),
  (∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)) →
    (nhds 1).HasBasis (fun x => True) V → LocallyCompactSpace (X →ₜ* Y)