Let k be given.
Assume HkO: k ∈ ω.
Set Dom to be the term setprod (Romega_tilde k) R.
We prove the intermediate claim Hcont: continuous_map Dom (product_topology (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)) R R_standard_topology) R_omega_space R_omega_product_topology (Romega_extend_map k).
An exact proof term for the current goal is (Romega_extend_map_continuous_in_Romega_product k HkO).
We prove the intermediate claim Hsub: Romega_tilde (ordsucc k) ⊆ R_omega_space.
An exact proof term for the current goal is (Romega_tilde_sub_Romega (ordsucc k)).
We prove the intermediate claim Himg: ∀p : set, p ∈ Dom → apply_fun (Romega_extend_map k) p ∈ Romega_tilde (ordsucc k).
Let p be given.
Assume Hp: p ∈ Dom.
rewrite the current goal using (Romega_extend_map_apply k p HkO Hp) (from left to right).
An exact proof term for the current goal is (Romega_extend_seq_in_Romega_tilde_succ k p HkO Hp).
An exact proof term for the current goal is (continuous_map_range_restrict Dom (product_topology (Romega_tilde k) (subspace_topology R_omega_space R_omega_product_topology (Romega_tilde k)) R R_standard_topology) R_omega_space R_omega_product_topology (Romega_extend_map k) (Romega_tilde (ordsucc k)) Hcont Hsub Himg).
∎