Let n be given.

Assume HnO: n ∈ ω.

Set X to be the term R_omega_space.

Set T to be the term R_omega_box_topology.

Set T' to be the term R_omega_product_topology.

Set Y to be the term Romega_tilde n.

We prove the intermediate claim HT: topology_on X T.

Set Xi to be the term const_space_family ω R R_standard_topology.

We prove the intermediate claim HXeq: X = product_space ω Xi.

Use reflexivity.

We prove the intermediate claim HTeq: T = box_topology ω Xi.

Use reflexivity.

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

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

Apply (box_topology_is_topology_on ω Xi) to the current goal.

Let i be given.

Assume Hi: i ∈ ω.

We will prove topology_on (space_family_set Xi i) (space_family_topology Xi i).

rewrite the current goal using (space_family_set_const_space_family ω R R_standard_topology i Hi) (from left to right).

rewrite the current goal using (space_family_topology_const_space_family ω R R_standard_topology i Hi) (from left to right).

An exact proof term for the current goal is R_standard_topology_is_topology_local.

We prove the intermediate claim HT': topology_on X T'.

An exact proof term for the current goal is Romega_product_topology_is_topology.

We prove the intermediate claim Hfiner: T' ⊆ T.

An exact proof term for the current goal is Romega_product_topology_sub_Romega_box_topology.

We prove the intermediate claim HYsubX: Y ⊆ X.

An exact proof term for the current goal is (Romega_tilde_sub_Romega n).

An exact proof term for the current goal is (ex16_2_finer_subspaces X T T' Y HT HT' Hfiner HYsubX).

∎