Let X, Tx and fn be given.

Assume HTx: topology_on X Tx.

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

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

Assume Huc: uniform_cauchy_metric X R R_bounded_metric fn.

We prove the intermediate claim Hexlim: ∃f : set, function_on f X R ∧ uniform_limit_metric X R R_bounded_metric fn f.

An exact proof term for the current goal is (uniform_cauchy_metric_complete_imp_uniform_limit_stub X R R_bounded_metric fn R_bounded_metric_complete_early Hfn Huc).

Apply Hexlim to the current goal.

Let f be given.

Assume Hfpack: function_on f X R ∧ uniform_limit_metric X R R_bounded_metric fn f.

We use f to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hfpack.

An exact proof term for the current goal is (uniform_limit_of_continuous_to_R_standard_topology X Tx fn f HTx Hfn (andEL (function_on f X R) (uniform_limit_metric X R R_bounded_metric fn f) Hfpack) Hcont (andER (function_on f X R) (uniform_limit_metric X R R_bounded_metric fn f) Hfpack)).

∎