Let X, Tx, Y and Ty be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Set Dom to be the term function_space X Y.
Set Tdom to be the term compact_convergence_topology X Tx Y Ty.
Set CXY to be the term continuous_function_space X Tx Y Ty.
We will prove topology_on CXY (compact_open_topology_C X Tx Y Ty).
We prove the intermediate claim HTdom: topology_on Dom Tdom.
An exact proof term for the current goal is (compact_convergence_topology_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim HCsub: CXY ⊆ Dom.
An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty).
An exact proof term for the current goal is (subspace_topology_is_topology Dom Tdom CXY HTdom HCsub).
∎