proposition: Lemma Fun_Series_Sum_wd' : (forall n, Feq I (f n) (g n)) -> Feq I (Fun_Series_Sum convF) (Fun_Series_Sum convG).
proof: Proof. intro H. apply eq_imp_Feq. Included. Included. intros x H0 Hx Hx'; simpl in |- *. apply series_sum_wd. intro; elim (H n); intros. inversion_clear b0; auto. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series