Let X, Tx, Y and Ty be given.

Assume HTx: topology_on X Tx.

Assume HTy: topology_on Y Ty.

We will prove continuous_map (setprod X Y) (product_topology X Tx Y Ty) X Tx (projection_map1 X Y) ∧ continuous_map (setprod X Y) (product_topology X Tx Y Ty) Y Ty (projection_map2 X Y).

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

∎