Let k be given.
Assume HkO: k ∈ ω.
Set A to be the term Romega_tilde (ordsucc k).
Set Ta to be the term subspace_topology R_omega_space R_omega_product_topology A.
Set X to be the term Romega_tilde k.
Set Tx to be the term subspace_topology R_omega_space R_omega_product_topology X.
We prove the intermediate claim HtopRomega: topology_on R_omega_space R_omega_product_topology.
An exact proof term for the current goal is Romega_product_topology_is_topology.
We prove the intermediate claim HA_sub: A ⊆ R_omega_space.
An exact proof term for the current goal is (Romega_tilde_sub_Romega (ordsucc k)).
We prove the intermediate claim HX_sub: X ⊆ R_omega_space.
An exact proof term for the current goal is (Romega_tilde_sub_Romega k).
We prove the intermediate claim HsuccO: ordsucc k ∈ ω.
An exact proof term for the current goal is (omega_ordsucc k HkO).
We prove the intermediate claim HcontRestrProd: continuous_map R_omega_space R_omega_product_topology R_omega_space R_omega_product_topology (Romega_restrict_map k).
An exact proof term for the current goal is (Romega_restrict_map_continuous_in_Romega_product k HkO).
We prove the intermediate claim HcontRestrA: continuous_map A Ta R_omega_space R_omega_product_topology (Romega_restrict_map k).
An exact proof term for the current goal is (continuous_on_subspace R_omega_space R_omega_product_topology R_omega_space R_omega_product_topology (Romega_restrict_map k) A HtopRomega HA_sub HcontRestrProd).
We prove the intermediate claim HimgRestr: ∀f : set, f ∈ A → apply_fun (Romega_restrict_map k) f ∈ X.
Let f be given.
Assume HfA: f ∈ A.
We prove the intermediate claim HfX: f ∈ R_omega_space.
An exact proof term for the current goal is (HA_sub f HfA).
rewrite the current goal using (Romega_restrict_map_apply k f HkO HfX) (from left to right).
An exact proof term for the current goal is (Romega_restrict_seq_in_Romega_tilde k f HkO HfX).
We prove the intermediate claim HcontRestrToX: continuous_map A Ta X Tx (Romega_restrict_map k).
An exact proof term for the current goal is (continuous_map_range_restrict A Ta R_omega_space R_omega_product_topology (Romega_restrict_map k) X HcontRestrA HX_sub HimgRestr).
We prove the intermediate claim HcontCoordProd: continuous_map R_omega_space R_omega_product_topology R R_standard_topology (Romega_coord_map (ordsucc k)).
An exact proof term for the current goal is (Romega_coord_map_continuous_in_Romega_product (ordsucc k) HsuccO).
We prove the intermediate claim HcontCoordA: continuous_map A Ta R R_standard_topology (Romega_coord_map (ordsucc k)).
An exact proof term for the current goal is (continuous_on_subspace R_omega_space R_omega_product_topology R R_standard_topology (Romega_coord_map (ordsucc k)) A HtopRomega HA_sub HcontCoordProd).
We prove the intermediate claim HpairCont: continuous_map A Ta (setprod X R) (product_topology X Tx R R_standard_topology) (pair_map A (Romega_restrict_map k) (Romega_coord_map (ordsucc k))).
An exact proof term for the current goal is (maps_into_products_axiom A Ta X Tx R R_standard_topology (Romega_restrict_map k) (Romega_coord_map (ordsucc k)) HcontRestrToX HcontCoordA).
We prove the intermediate claim Heq: pair_map A (Romega_restrict_map k) (Romega_coord_map (ordsucc k)) = Romega_split_map k.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ pair_map A (Romega_restrict_map k) (Romega_coord_map (ordsucc k)).
We will prove p ∈ Romega_split_map k.
Apply (ReplE_impred A (λa0 : set ⇒ (a0,(apply_fun (Romega_restrict_map k) a0,apply_fun (Romega_coord_map (ordsucc k)) a0))) p Hp (p ∈ Romega_split_map k)) to the current goal.
Let a be given.
Assume Ha: a ∈ A.
Assume Heqp: p = (a,(apply_fun (Romega_restrict_map k) a,apply_fun (Romega_coord_map (ordsucc k)) a)).
We prove the intermediate claim HaX: a ∈ R_omega_space.
An exact proof term for the current goal is (HA_sub a Ha).
We prove the intermediate claim Hra: apply_fun (Romega_restrict_map k) a = Romega_restrict_seq k a.
An exact proof term for the current goal is (Romega_restrict_map_apply k a HkO HaX).
We prove the intermediate claim Hca: apply_fun (Romega_coord_map (ordsucc k)) a = apply_fun a (ordsucc k).
An exact proof term for the current goal is (Romega_coord_map_apply (ordsucc k) a HsuccO HaX).
rewrite the current goal using Heqp (from left to right).
rewrite the current goal using Hra (from left to right).
rewrite the current goal using Hca (from left to right).
An exact proof term for the current goal is (ReplI A (λf0 : set ⇒ (f0,(Romega_restrict_seq k f0,apply_fun f0 (ordsucc k)))) a Ha).
Let p be given.
Assume Hp: p ∈ Romega_split_map k.
We will prove p ∈ pair_map A (Romega_restrict_map k) (Romega_coord_map (ordsucc k)).
We prove the intermediate claim Hdef: Romega_split_map k = graph A (λf0 : set ⇒ (Romega_restrict_seq k f0,apply_fun f0 (ordsucc k))).
Use reflexivity.
We prove the intermediate claim Hp2: p ∈ graph A (λf0 : set ⇒ (Romega_restrict_seq k f0,apply_fun f0 (ordsucc k))).
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is Hp.
Apply (ReplE_impred A (λf0 : set ⇒ (f0,(Romega_restrict_seq k f0,apply_fun f0 (ordsucc k)))) p Hp2 (p ∈ pair_map A (Romega_restrict_map k) (Romega_coord_map (ordsucc k)))) to the current goal.
Let a be given.
Assume Ha: a ∈ A.
Assume Heqp: p = (a,(Romega_restrict_seq k a,apply_fun a (ordsucc k))).
We prove the intermediate claim HaX: a ∈ R_omega_space.
An exact proof term for the current goal is (HA_sub a Ha).
We prove the intermediate claim Hra: apply_fun (Romega_restrict_map k) a = Romega_restrict_seq k a.
An exact proof term for the current goal is (Romega_restrict_map_apply k a HkO HaX).
We prove the intermediate claim Hca: apply_fun (Romega_coord_map (ordsucc k)) a = apply_fun a (ordsucc k).
An exact proof term for the current goal is (Romega_coord_map_apply (ordsucc k) a HsuccO HaX).
rewrite the current goal using Heqp (from left to right).
rewrite the current goal using Hra (from right to left).
rewrite the current goal using Hca (from right to left).
An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ (a0,(apply_fun (Romega_restrict_map k) a0,apply_fun (Romega_coord_map (ordsucc k)) a0))) a Ha).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HpairCont.
∎