Let seq be given.
Assume Hseq: sequence_on seq R.
Assume HabC: ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → abs_SNo (add_SNo (apply_fun seq m) (minus_SNo (apply_fun seq n))) < eps.
We prove the intermediate claim HexStd: ∃x : set, converges_to R R_standard_topology seq x.
An exact proof term for the current goal is (abs_Cauchy_sequence_converges_R_standard_topology seq Hseq HabC).
Apply HexStd to the current goal.
Let x be given.
Assume HxStd: converges_to R R_standard_topology seq x.
We use x to witness the existential quantifier.
We will prove converges_to R (metric_topology R R_bounded_metric) seq x.
rewrite the current goal using metric_topology_R_bounded_metric_eq_R_standard_topology (from left to right).
An exact proof term for the current goal is HxStd.
∎