Let f be given.

Assume Hf: f ∈ Romega_infty.

We will prove f ∈ R_omega_space.

Apply (UnionE_impred {Romega_tilde n|n ∈ ω} f Hf) to the current goal.

Let Y be given.

Assume HfY: f ∈ Y.

Assume HY: Y ∈ {Romega_tilde n|n ∈ ω}.

Apply (ReplE_impred ω (λn : set ⇒ Romega_tilde n) Y HY (f ∈ R_omega_space)) to the current goal.

Let n be given.

Assume Hn: n ∈ ω.

Assume HYeq: Y = Romega_tilde n.

We prove the intermediate claim HfY2: f ∈ Romega_tilde n.

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

An exact proof term for the current goal is HfY.

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

∎