Let n be given.

Assume HnO: n ∈ ω.

We will prove metrizable (Romega_tilde n) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde n)).

An exact proof term for the current goal is (subspace_of_metrizable_is_metrizable R_omega_space R_omega_product_topology (Romega_tilde n) Romega_product_topology_metrizable (Romega_tilde_sub_Romega n)).

∎