We will prove normal_space S_Omega SOmega_topology ∧ normal_space Sbar_Omega SbarOmega_topology ∧ ¬ normal_space (setprod S_Omega Sbar_Omega) (product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology).

Apply andI to the current goal.

An exact proof term for the current goal is SOmega_SbarOmega_factors_normal.

An exact proof term for the current goal is SOmega_SbarOmega_product_not_normal.

∎