proposition: Lemma Cauchy_fun_seq_seq2 : Cauchy_fun_seq -> Cauchy_fun_seq2.
proof: Proof. intro H. red in |- *; red in H. intros e H0. elim (H e H0); intros N HN; exists N. intros; apply HN; auto with arith. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval