proposition: Lemma FSeries_Sum_plus : forall H : fun_series_convergent_IR J (fun n => f n{+}g n), Feq J (FSeries_Sum H) (FSeries_Sum convF{+}FSeries_Sum convG).
proof: Proof. intros. apply included_Feq'; intros a b Hab H0. eapply Feq_transitive. apply (FSeries_Sum_char _ _ H a b Hab H0). eapply Feq_transitive. apply Fun_Series_Sum_plus with (convF := convF a b Hab H0) (convG := convG a b Hab H0). apply Feq_symmetric; apply Feq_plus; apply FSeries_Sum_char. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions