∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b c : α}
  [inst_3 : Fact (a ≤ b)] [inst_4 : Fact (b ≤ c)] {E : Type u_2} [inst_5 : TopologicalSpace E]
  {f : C(↑(Set.Icc a b), E)} {g : C(↑(Set.Icc b c), E)},
  f ⊤ = g ⊥ → ∀ {t : ↑(Set.Icc a c)} (ht : ↑t ≤ b), (f.concat g) t = f ⟨↑t, ⋯⟩