proposition: Lemma conv_Cauchy_fun_seq'_IR : conv_fun_seq'_IR -> Cauchy_fun_seq_IR.
proof: Proof. intro H. red in |- *; red in H. intros. apply conv_Cauchy_fun_seq' with F (included_imp_Continuous _ _ contF _ _ _ Hinc); auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions