Let X, Y, Ty, F and a be given.

Assume HaX: a ∈ X.

rewrite the current goal using (space_family_topology_def (Ascoli_XiKa X Y Ty F) a) (from left to right).

We prove the intermediate claim HXiDef: Ascoli_XiKa X Y Ty F = graph X (λa0 : set ⇒ (closure_of Y Ty (Ascoli_F_at X Y a0 F),subspace_topology Y Ty (closure_of Y Ty (Ascoli_F_at X Y a0 F)))).

Use reflexivity.

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

rewrite the current goal using (apply_fun_graph X (λa0 : set ⇒ (closure_of Y Ty (Ascoli_F_at X Y a0 F),subspace_topology Y Ty (closure_of Y Ty (Ascoli_F_at X Y a0 F)))) a HaX) (from left to right).

An exact proof term for the current goal is (tuple_2_1_eq (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)))).

∎