Let X, Tx, Y, dY and F be given.
Assume Htop: topology_on (function_space X Y) (pointwise_convergence_topology X Tx Y (metric_topology Y dY)).
Set Dom to be the term function_space X Y.
Set Tpt to be the term pointwise_convergence_topology X Tx Y (metric_topology Y dY).
We will prove Ascoli_g_pointwise_closure X Tx Y dY F ⊆ Dom.
An exact proof term for the current goal is (closure_in_space Dom Tpt F Htop).
∎