proposition: Lemma convergent_imp_Continuous : fun_series_convergent_IR J f -> forall n, Continuous J (f n).
proof: Proof. intros H n. split. exact (convergent_imp_inc H n). intros a b Hab H0; auto. elim (H a b Hab H0); auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions