Let X, Tx, Y, Ty and y0 be given.
Assume HX: connected_space X Tx.
Assume HTy: topology_on Y Ty.
Assume Hy0: y0 ∈ Y.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (¬ (∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V)) HX).
Set idX to be the term {(x,x)|x ∈ X}.
Set c to be the term const_fun X y0.
Set f to be the term pair_map X idX c.
We prove the intermediate claim Hid: continuous_map X Tx X Tx idX.
An exact proof term for the current goal is (identity_continuous X Tx HTx).
We prove the intermediate claim Hc: continuous_map X Tx Y Ty c.
An exact proof term for the current goal is (const_fun_continuous X Tx Y Ty y0 HTx HTy Hy0).
We prove the intermediate claim Hf: continuous_map X Tx (setprod X Y) (product_topology X Tx Y Ty) f.
An exact proof term for the current goal is (maps_into_products X Tx X Tx Y Ty idX c Hid Hc).
We prove the intermediate claim Himg: connected_space (image_of f X) (subspace_topology (setprod X Y) (product_topology X Tx Y Ty) (image_of f X)).
An exact proof term for the current goal is (continuous_image_connected X Tx (setprod X Y) (product_topology X Tx Y Ty) f HX Hf).
We will prove connected_space (setprod X {y0}) (subspace_topology (setprod X Y) (product_topology X Tx Y Ty) (setprod X {y0})).
rewrite the current goal using (image_of_id_const_is_slice X y0) (from right to left).
An exact proof term for the current goal is Himg.
∎