Apply andI to the current goal.

An exact proof term for the current goal is (xm (normal_space R_omega_space R_omega_product_topology)).

An exact proof term for the current goal is (xm (normal_space real_sequences uniform_topology)).

∎