∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] [inst_3 : DiscreteTopology δ] (f f_1 : α ↪ δ),
  f = f_1 →
    ∀ (g g_1 : BoundedContinuousFunction α β),
      g = g_1 →
        ∀ (h h_1 : BoundedContinuousFunction δ β),
          h = h_1 → BoundedContinuousFunction.extend f g h = BoundedContinuousFunction.extend f_1 g_1 h_1