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)).
Assume HFsub: F ⊆ function_space X Y.
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 closed_in Dom Tpt (Ascoli_g_pointwise_closure X Tx Y dY F).
An exact proof term for the current goal is (closure_is_closed Dom Tpt F Htop HFsub).
∎