proposition: Lemma fun_series_conv : forall H H', conv_fun_seq' a b Hab (fun_seq_part_sum f) (Fun_Series_Sum convF) H H'.
proof: Proof. intros. inversion_clear convF. try rename X into H0. apply conv_fun_seq'_wdr with (contf := fun_seq_part_sum_cont _ _ _ _ x) (contF := Cauchy_cont_Lim _ _ _ _ _ H0). 2: apply Cauchy_conv_fun_seq'. apply Feq_symmetric; apply Fun_Series_Sum_char'. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series