proposition: Lemma Fun_Series_Sum_cont : Continuous_I Hab (Fun_Series_Sum convF).
proof: Proof. intros. inversion_clear convF. try rename X into H. eapply Continuous_I_wd. apply Feq_symmetric; apply (Fun_Series_Sum_char' (fun n : nat => fun_seq_part_sum_cont _ _ _ _ x n) H). Contin. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series