Let X, Tx, Y, dY, F and g be given.

Assume HTx: topology_on X Tx.

Assume HdY: metric_on Y dY.

Assume HFsubC: F ⊆ continuous_function_space X Tx Y (metric_topology Y dY).

Assume Hequi: equicontinuous_family X Tx Y dY F.

Assume Hgcl: g ∈ Ascoli_g_pointwise_closure X Tx Y dY F.

Set Ty to be the term metric_topology Y dY.

Set CXY to be the term continuous_function_space X Tx Y Ty.

We prove the intermediate claim HTy: topology_on Y Ty.

An exact proof term for the current goal is (metric_topology_is_topology Y dY HdY).

We prove the intermediate claim HTpt: topology_on (function_space X Y) (pointwise_convergence_topology X Tx Y Ty).

An exact proof term for the current goal is (pointwise_convergence_topology_is_topology X Tx Y Ty HTx HTy).

We prove the intermediate claim HgFS: g ∈ function_space X Y.

An exact proof term for the current goal is (Ascoli_g_pointwise_closure_sub X Tx Y dY F HTpt g Hgcl).

We prove the intermediate claim HCXYdef: continuous_function_space X Tx Y Ty = {f ∈ function_space X Y|continuous_map X Tx Y Ty f}.

Use reflexivity.

rewrite the current goal using HCXYdef (from left to right).

An exact proof term for the current goal is (SepI (function_space X Y) (λf0 : set ⇒ continuous_map X Tx Y Ty f0) g HgFS (Ascoli_g_pointwise_closure_continuous_map X Tx Y dY F g HTx HdY HFsubC Hequi Hgcl)).

∎