Set h to be the term const_fun unit_interval 0.
We prove the intermediate claim Hh: continuous_map unit_interval I_topology R R_standard_topology h.
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).
We prove the intermediate claim Hex: ∃g : set, continuous_map unit_interval I_topology R R_standard_topology g ∧ nowhere_differentiable g ∧ ∀x : set, x ∈ unit_interval → Rlt (Abs (add_SNo (apply_fun h x) (minus_SNo (apply_fun g x)))) 1.
An exact proof term for the current goal is (theorem_49_1_nowhere_differentiable_approx h 1 Hh real_1 Rlt_0_1).
Set g to be the term Eps_i (λg0 : set ⇒ continuous_map unit_interval I_topology R R_standard_topology g0 ∧ nowhere_differentiable g0 ∧ ∀x : set, x ∈ unit_interval → Rlt (Abs (add_SNo (apply_fun h x) (minus_SNo (apply_fun g0 x)))) 1).
We prove the intermediate claim HgP: continuous_map unit_interval I_topology R R_standard_topology g ∧ nowhere_differentiable g ∧ ∀x : set, x ∈ unit_interval → Rlt (Abs (add_SNo (apply_fun h x) (minus_SNo (apply_fun g x)))) 1.
An exact proof term for the current goal is (Eps_i_ex (λg0 : set ⇒ continuous_map unit_interval I_topology R R_standard_topology g0 ∧ nowhere_differentiable g0 ∧ ∀x : set, x ∈ unit_interval → Rlt (Abs (add_SNo (apply_fun h x) (minus_SNo (apply_fun g0 x)))) 1) Hex).
We prove the intermediate claim HgCN: continuous_map unit_interval I_topology R R_standard_topology g ∧ nowhere_differentiable g.
An exact proof term for the current goal is (andEL (continuous_map unit_interval I_topology R R_standard_topology g ∧ nowhere_differentiable g) (∀x : set, x ∈ unit_interval → Rlt (Abs (add_SNo (apply_fun h x) (minus_SNo (apply_fun g x)))) 1) HgP).
We use g to witness the existential quantifier.
An exact proof term for the current goal is HgCN.
∎