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 (setprod X Y) (product_topology X Tx Y Ty).

An exact proof term for the current goal is (lemma_topology_from_basis (setprod X Y) (product_subbasis X Tx Y Ty) (product_subbasis_is_basis X Tx Y Ty HTx HTy)).

∎