proposition: Lemma Continuous_FSeries_Sum : forall H, Continuous J (FSeries_Sum (J:=J) (f:=f) H).
proof: Proof. intros. split; Included. intros a b Hab H0. eapply Continuous_I_wd. apply Feq_symmetric; apply (FSeries_Sum_char _ _ H _ _ _ H0). eapply Continuous_I_wd. apply Fun_Series_Sum_char. apply Cauchy_cont_Lim. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions