proposition: Lemma FSeries_Sum_comp_conv : fun_series_convergent_IR I (fun n => g n[o]F).
proof: Proof. red in |- *; intros. destruct (Hmap a b Hab Hinc) as [c [d [Hcd [H0 H1]]]]. apply conv_fun_series_comp with c d Hcd; auto. eapply included_imp_Continuous. apply contF. auto. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries