We will prove continuous_map R R_standard_topology unit_interval unit_interval_topology normalize01_fun.

We prove the intermediate claim HcontR: continuous_map R R_standard_topology R R_standard_topology normalize01_fun.

An exact proof term for the current goal is normalize01_fun_continuous.

We prove the intermediate claim Hut: unit_interval_topology = subspace_topology R R_standard_topology unit_interval.

Use reflexivity.

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

Apply (continuous_map_range_restrict R R_standard_topology R R_standard_topology normalize01_fun unit_interval HcontR unit_interval_sub_R) to the current goal.

Let x be given.

Assume HxR: x ∈ R.

An exact proof term for the current goal is (normalize01_fun_range_in_unit_interval x HxR).

∎