Let X, Tx, fn and f be given.

Assume HTx: topology_on X Tx.

Assume Hfn: function_on fn ω (function_space X R).

Assume Hf: function_on f X R.

Assume Hcont: ∀n : set, n ∈ ω → continuous_map X Tx R R_standard_topology (apply_fun fn n).

Assume Hunif: uniform_limit_metric X R R_bounded_metric fn f.

We will prove continuous_map X Tx R R_standard_topology f.

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

We prove the intermediate claim Hcont2: ∀n : set, n ∈ ω → continuous_map X Tx R (metric_topology R R_bounded_metric) (apply_fun fn n).

Let n be given.

Assume HnO: n ∈ ω.

We will prove continuous_map X Tx R (metric_topology R R_bounded_metric) (apply_fun fn n).

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

An exact proof term for the current goal is (Hcont n HnO).

An exact proof term for the current goal is (uniform_limit_of_continuous_to_metric_is_continuous X Tx R R_bounded_metric fn f HTx R_bounded_metric_is_metric_on_early Hfn Hf Hcont2 Hunif).

∎