Let X, Y, dY and F be given.
Assume HdY: metric_on Y dY.
Assume Hpwc: Ascoli_pointwise_compact_closure X Y dY F.
Set Ty to be the term metric_topology Y dY.
We prove the intermediate claim Hcomp: ∀a : set, a ∈ X → compact_space (product_component (Ascoli_XiKa X Y Ty F) a) (product_component_topology (Ascoli_XiKa X Y Ty F) a).
Let a be given.
Assume HaX: a ∈ X.
We prove the intermediate claim HKa: compact_space (closure_of Y Ty (Ascoli_F_at X Y a F)) (subspace_topology Y Ty (closure_of Y Ty (Ascoli_F_at X Y a F))).
An exact proof term for the current goal is (Hpwc a HaX).
rewrite the current goal using (space_family_set_eq_product_component (Ascoli_XiKa X Y Ty F) a) (from right to left).
rewrite the current goal using (space_family_topology_eq_product_component_topology (Ascoli_XiKa X Y Ty F) a) (from right to left).
rewrite the current goal using (Ascoli_XiKa_set X Y Ty F a HaX) (from left to right).
rewrite the current goal using (Ascoli_XiKa_topology X Y Ty F a HaX) (from left to right).
An exact proof term for the current goal is HKa.
An exact proof term for the current goal is (Tychonoff_theorem X (Ascoli_XiKa X Y Ty F) Hcomp).
∎