proposition: Lemma FSeries_Sum_scal_conv : fun_series_convergent_IR J (fun n => H{*}f n).
proof: Proof. red in |- *; intros. apply conv_fun_series_scal; auto. eapply included_imp_Continuous. apply contH. auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions