proposition: Lemma fun_series_convergent_wd : (forall n, Feq I (f n) (g n)) -> fun_series_convergent _ _ Hab f -> fun_series_convergent _ _ Hab g.
proof: Proof. intros H H0. elim H0; intros contF convF. cut (forall n : nat, Continuous_I Hab (g n)). intro H1. exists H1. apply Cauchy_fun_seq_wd with (fun_seq_part_sum f) (fun_seq_part_sum_cont _ _ _ _ contF). 2: assumption. intros. apply eq_imp_Feq. apply contin_imp_inc; Contin. apply contin_imp_inc; Contin. intros x H2 Hx Hx'; simpl in |- *. apply Sum0_wd. intro i; elim (H i); intros. inversion_clear b0; auto. intro; apply Continuous_I_wd with (f n); auto. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series