We prove the intermediate claim Hf: continuous_real_on_I ex49_example1_f.
An exact proof term for the current goal is (SepE2 (function_space unit_interval R) (λf0 : set ⇒ continuous_real_on_I f0) ex49_example1_f ex49_example1_f_in_C_I_R).
We prove the intermediate claim Hg: continuous_real_on_I ex49_example1_g.
An exact proof term for the current goal is (SepE2 (function_space unit_interval R) (λg0 : set ⇒ continuous_real_on_I g0) ex49_example1_g ex49_example1_g_in_C_I_R).
We prove the intermediate claim Hk: continuous_real_on_I ex49_example1_k.
An exact proof term for the current goal is (SepE2 (function_space unit_interval R) (λk0 : set ⇒ continuous_real_on_I k0) ex49_example1_k ex49_example1_k_in_C_I_R).
We will prove (continuous_map unit_interval I_topology R R_standard_topology ex49_example1_f ∧ continuous_map unit_interval I_topology R R_standard_topology ex49_example1_g) ∧ continuous_map unit_interval I_topology R R_standard_topology ex49_example1_k.
Apply andI to the current goal.
We will prove continuous_map unit_interval I_topology R R_standard_topology ex49_example1_f ∧ continuous_map unit_interval I_topology R R_standard_topology ex49_example1_g.
Apply andI to the current goal.
An exact proof term for the current goal is Hf.
An exact proof term for the current goal is Hg.
An exact proof term for the current goal is Hk.
∎