Let X, Tx, g and h be given.

Assume HTx: topology_on X Tx.

Assume Hg: continuous_map X Tx R R_standard_topology g.

Assume Hh: continuous_map X Tx R R_standard_topology h.

We will prove continuous_map X Tx R R_standard_topology (compose_fun X (pair_map X g h) add_fun_R).

Set p to be the term pair_map X g h.

We prove the intermediate claim Hpcont: continuous_map X Tx (setprod R R) (product_topology R R_standard_topology R R_standard_topology) p.

An exact proof term for the current goal is (maps_into_products_axiom X Tx R R_standard_topology R R_standard_topology g h Hg Hh).

We prove the intermediate claim Haddcont: continuous_map (setprod R R) (product_topology R R_standard_topology R R_standard_topology) R R_standard_topology add_fun_R.

An exact proof term for the current goal is add_fun_R_continuous.

An exact proof term for the current goal is (composition_continuous X Tx (setprod R R) (product_topology R R_standard_topology R R_standard_topology) R R_standard_topology p add_fun_R Hpcont Haddcont).

∎