Let A, Ta, X, Tx, Y, Ty, f and g be given.

Assume Hf: continuous_map A Ta X Tx f.

Assume Hg: continuous_map A Ta Y Ty g.

We will prove continuous_map A Ta (setprod X Y) (product_topology X Tx Y Ty) (pair_map A f g).

An exact proof term for the current goal is (maps_into_products_axiom A Ta X Tx Y Ty f g Hf Hg).

∎