We will prove topology_on R_omega_space uniform_topology.

rewrite the current goal using (real_sequences_eq_Romega_space) (from right to left).

An exact proof term for the current goal is uniform_topology_is_topology.

∎