Set f0 to be the term const_fun unit_interval 0.

We use f0 to witness the existential quantifier.

We will prove f0 ∈ C_I_R.

Apply (SepI (function_space unit_interval R) (λf1 : set ⇒ continuous_real_on_I f1) f0) to the current goal.

We will prove f0 ∈ function_space unit_interval R.

We prove the intermediate claim Hpow: f0 ∈ 𝒫 (setprod unit_interval R).

We will prove f0 ∈ 𝒫 (setprod unit_interval R).

Apply (PowerI (setprod unit_interval R) f0) to the current goal.

Let p be given.

Assume Hp: p ∈ f0.

We will prove p ∈ setprod unit_interval R.

Apply (ReplE_impred unit_interval (λa : set ⇒ (a,0)) p Hp (p ∈ setprod unit_interval R)) to the current goal.

Let a be given.

Assume Ha: a ∈ unit_interval.

Assume Heq: p = (a,0).

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma unit_interval R a 0 Ha real_0).

We prove the intermediate claim Hfun: function_on f0 unit_interval R.

Let x be given.

Assume Hx: x ∈ unit_interval.

We will prove apply_fun f0 x ∈ R.

rewrite the current goal using (const_fun_apply unit_interval 0 x Hx) (from left to right).

An exact proof term for the current goal is real_0.

An exact proof term for the current goal is (SepI (𝒫 (setprod unit_interval R)) (λf : set ⇒ function_on f unit_interval R) f0 Hpow Hfun).

We will prove continuous_real_on_I f0.

An exact proof term for the current goal is (const_fun_continuous unit_interval I_topology R R_standard_topology 0 I_topology_on R_standard_topology_is_topology real_0).

∎