proposition: Lemma FSeries_Sum_comp : forall H' : fun_series_convergent_IR I (fun n => g n[o]F), Feq I (FSeries_Sum H') (FSeries_Sum convG[o]F).
proof: Proof. intros. apply included_Feq'; intros a b Hab Hinc. destruct (Hmap a b Hab Hinc) as [c [d [Hcd [H0 H1]]]]. assert (H2:Continuous_I Hab F). eapply included_imp_Continuous. apply contF. auto. eapply Feq_transitive. apply (FSeries_Sum_char _ _ H' a b Hab Hinc). apply Feq_transitive with (Fun_Series_Sum (a:=c) (b:=d) (Hab:=Hcd) (f:=g) (convG _ _ _ H0)[o]F). apply Fun_Series_Sum_comp. auto. apply H1. eapply Feq_comp; try apply H1. apply Feq_reflexive. Included. apply Feq_symmetric. apply FSeries_Sum_char. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries