Let A, Ta, X, Tx, Y, Ty and h be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume Hfunh: function_on h A (setprod X Y).
Apply iffI to the current goal.
Assume Hh: continuous_map A Ta (setprod X Y) (product_topology X Tx Y Ty) h.
An exact proof term for the current goal is (maps_into_products_converse A Ta X Tx Y Ty h HTx HTy Hh).
Assume Hcoords: 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 Hc1: continuous_map A Ta X Tx (compose_fun A h (projection_map1 X Y)).
An exact proof term for the current goal is (andEL (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))) Hcoords).
We prove the intermediate claim Hc2: continuous_map A Ta Y Ty (compose_fun A h (projection_map2 X Y)).
An exact proof term for the current goal is (andER (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))) Hcoords).
An exact proof term for the current goal is (maps_into_products_coords_imp A Ta X Tx Y Ty h HTx HTy Hfunh Hc1 Hc2).
∎