proposition: Lemma Cauchy_fun_seq'_seq1 : Cauchy_fun_seq' -> Cauchy_fun_seq1.
proof: Proof. intro H. red in |- *; red in H. intro. elim (H k); clear H; intros N HN. exists N; intros. apply leEq_Norm_Funct. intros x H1 Hx. eapply leEq_wdl. apply (HN m n H H0 x H1). apply AbsIR_wd; simpl in |- *; rational. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval