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