Let X, Tx, Y and Ty be given.
Let f be given.
Assume Hf: f ∈ continuous_function_space X Tx Y Ty.
We will prove f ∈ function_space X Y.
An exact proof term for the current goal is (SepE1 (function_space X Y) (λg : set ⇒ continuous_map X Tx Y Ty g) f Hf).
∎