We will prove Romega_product_topology_on_real_sequences = R_omega_product_topology.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set T to be the term product_topology_full ω Xi.
We prove the intermediate claim HTdef: R_omega_product_topology = T.
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
We prove the intermediate claim HdefL: Romega_product_topology_on_real_sequences = subspace_topology R_omega_space T real_sequences.
Use reflexivity.
rewrite the current goal using HdefL (from left to right).
rewrite the current goal using (real_sequences_eq_Romega_space) (from left to right).
We prove the intermediate claim HT: topology_on R_omega_space T.
rewrite the current goal using HTdef (from right to left).
An exact proof term for the current goal is Romega_product_topology_is_topology.
An exact proof term for the current goal is (subspace_topology_whole R_omega_space T HT).
∎