Let X, dX, Y, dY, f_seq and f be given.
Assume H: uniform_convergence_functions X dX Y dY f_seq f.
We prove the intermediate claim HABCDE: ((((metric_on X dX ∧ metric_on Y dY) ∧ function_on f_seq ω (function_space X Y)) ∧ function_on f X Y) ∧ (∀n : set, n ∈ ω → function_on (apply_fun f_seq n) X Y)).
An exact proof term for the current goal is (andEL ((((metric_on X dX ∧ metric_on Y dY) ∧ function_on f_seq ω (function_space X Y)) ∧ function_on f X Y) ∧ (∀n : set, n ∈ ω → function_on (apply_fun f_seq n) X Y)) (∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → ∀x : set, x ∈ X → Rlt (apply_fun dY (apply_fun (apply_fun f_seq n) x,apply_fun f x)) eps) H).
We prove the intermediate claim HABCD: (((metric_on X dX ∧ metric_on Y dY) ∧ function_on f_seq ω (function_space X Y)) ∧ function_on f X Y).
An exact proof term for the current goal is (andEL (((metric_on X dX ∧ metric_on Y dY) ∧ function_on f_seq ω (function_space X Y)) ∧ function_on f X Y) (∀n : set, n ∈ ω → function_on (apply_fun f_seq n) X Y) HABCDE).
An exact proof term for the current goal is (andER (metric_on X dX ∧ metric_on Y dY) (function_on f_seq ω (function_space X Y)) (andEL (metric_on X dX ∧ metric_on Y dY ∧ function_on f_seq ω (function_space X Y)) (function_on f X Y) HABCD)).
∎