∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : PseudoEMetricSpace β] [inst_1 : Finite ↑𝔖]
  {f g : UniformOnFun α β 𝔖},
  edist f g =
    edist (UniformFun.ofFun ((⋃₀ 𝔖).restrict ((UniformOnFun.toFun 𝔖) f)))
      (UniformFun.ofFun ((⋃₀ 𝔖).restrict ((UniformOnFun.toFun 𝔖) g)))