Let A, Ta, X, Tx, Y, Ty and h be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume Hh: continuous_map A Ta (setprod X Y) (product_topology X Tx Y Ty) h.
We will prove continuous_map A Ta X Tx (compose_fun A h (projection_map1 X Y)) ∧ continuous_map A Ta Y Ty (compose_fun A h (projection_map2 X Y)).
We prove the intermediate claim Hproj: 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).
Apply andI to the current goal.
We prove the intermediate claim Hpr1: continuous_map (setprod X Y) (product_topology X Tx Y Ty) X Tx (projection_map1 X Y).
An exact proof term for the current goal is (andEL (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)) Hproj).
An exact proof term for the current goal is (composition_continuous A Ta (setprod X Y) (product_topology X Tx Y Ty) X Tx h (projection_map1 X Y) Hh Hpr1).
We prove the intermediate claim Hpr2: 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 (andER (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)) Hproj).
An exact proof term for the current goal is (composition_continuous A Ta (setprod X Y) (product_topology X Tx Y Ty) Y Ty h (projection_map2 X Y) Hh Hpr2).
∎