proposition: Lemma fun_series_conv_imp_conv : fun_series_convergent -> forall x, I x -> forall Hx, convergent (fun n => f n x (Hx n)).
proof: Proof. intros H x H0 Hx e He. elim H; intros incF convF. elim (convF _ He). intros N HN. exists N; intros. apply AbsIR_imp_AbsSmall. simpl in HN. eapply leEq_wdl. apply (HN m N H1 (le_n N) x H0). apply AbsIR_wd. apply cg_minus_wd; unfold seq_part_sum in |- *; apply Sum0_wd; intros; rational. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series