∀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀]
  [inst_2 : MulAction G₀ α] [ContinuousConstSMul G₀ α] [inst_4 : TopologicalSpace β] {f : β → α} {c : G₀} {s : Set β},
  c ≠ 0 → (ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s)