src/HOL/Library/Product_Vector.thy

   show "eventually (\<lambda>x. (f x, g x) \<in> S) net"
     by (rule eventually_elim2)
        (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
 qed
 
-lemma LIMSEQ_fst: "(X ----> a) \<Longrightarrow> (\<lambda>n. fst (X n)) ----> fst a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_fst)
-
-lemma LIMSEQ_snd: "(X ----> a) \<Longrightarrow> (\<lambda>n. snd (X n)) ----> snd a"
-unfolding LIMSEQ_conv_tendsto by (rule tendsto_snd)
-
-lemma LIMSEQ_Pair:
-  assumes "X ----> a" and "Y ----> b"
-  shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
-using assms unfolding LIMSEQ_conv_tendsto
-by (rule tendsto_Pair)
-
 lemma LIM_fst: "f -- x --> a \<Longrightarrow> (\<lambda>x. fst (f x)) -- x --> fst a"
 unfolding LIM_conv_tendsto by (rule tendsto_fst)
 
 lemma LIM_snd: "f -- x --> a \<Longrightarrow> (\<lambda>x. snd (f x)) -- x --> snd a"
 unfolding LIM_conv_tendsto by (rule tendsto_snd)

     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   have 2: "(\<lambda>n. snd (X n)) ----> lim (\<lambda>n. snd (X n))"
     using Cauchy_snd [OF `Cauchy X`]
     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   have "X ----> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
-    using LIMSEQ_Pair [OF 1 2] by simp
+    using tendsto_Pair [OF 1 2] by simp
   then show "convergent X"
     by (rule convergentI)
 qed
 
 subsection {* Product is a normed vector space *}