proposition: Lemma seq_conv_imp_fun_conv : forall x y, Cauchy_Lim_prop2 x y -> forall Hf HF, conv_fun_seq' a b Hab (fun n => [-C-] (x n)) [-C-]y Hf HF.
proof: Proof. intros x y H Hf HF e H0. elim (H e H0); intros N HN. exists N; intros; simpl in |- *. apply AbsSmall_imp_AbsIR. auto. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval