Let X, Tx, Y and Ty be given.

Assume HTx: topology_on X Tx.

Assume HTy: topology_on Y Ty.

We will prove topology_on (function_space X Y) (compact_convergence_topology X Tx Y Ty).

Set S to be the term compact_open_subbasis X Tx Y Ty.

We prove the intermediate claim HS: subbasis_on (function_space X Y) S.

An exact proof term for the current goal is (compact_open_subbasis_is_subbasis X Tx Y Ty HTx HTy).

An exact proof term for the current goal is (topology_from_subbasis_is_topology (function_space X Y) S HS).

∎