proposition: Lemma FSeries_Sum_scal : forall H' : fun_series_convergent_IR J (fun n => H{*}f n), Feq J (FSeries_Sum H') (H{*}FSeries_Sum convF).
proof: Proof. intros. apply included_Feq'; intros a b Hab H0. cut (Continuous_I Hab H). intro H1. eapply Feq_transitive. apply (FSeries_Sum_char _ _ H' a b Hab H0). eapply Feq_transitive. apply Fun_Series_Sum_scal with (convF := convF a b Hab H0). auto. apply Feq_symmetric; apply Feq_mult. apply Feq_reflexive; Included. apply FSeries_Sum_char. eapply included_imp_Continuous. apply contH. auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions