Let X, Tx, Y, dY and F 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.
Let g be given.
Assume Hg: g ∈ Ascoli_g_pointwise_closure X Tx Y dY F.
An exact proof term for the current goal is (Ascoli_g_pointwise_closure_sub_CXY X Tx Y dY F g HTx HdY HFsubC Hequi Hg).
∎