We will prove bounded_sequences_Romega ∈ 𝒫 R_omega_space.

Apply PowerI to the current goal.

Let f be given.

Assume Hf: f ∈ bounded_sequences_Romega.

We will prove f ∈ R_omega_space.

An exact proof term for the current goal is (SepE1 R_omega_space (λf0 : set ⇒ bounded_sequence_Romega f0) f Hf).

∎