∀ {α : Type u_2} {β : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α]
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [T0Space β] (f : α →+ β),
  UniformContinuous ⇑f →
    ∀ (a b : α),
      UniformSpace.Completion.extension (⇑f) (↑a + ↑b) =
        UniformSpace.Completion.extension ⇑f ↑a + UniformSpace.Completion.extension ⇑f ↑b