proposition: Lemma Fun_Series_Sum_as_Lim : forall Hf H', conv_fun_seq' _ _ Hab (fun_seq_part_sum f) (Fun_Series_Sum convF) Hf H'.
proof: Proof. intros. apply conv_fun_seq'_wdr with (fun_seq_part_sum_cont _ _ _ _ (ProjT1 convF)) (Cauchy_fun_seq_Lim _ _ _ _ _ (ProjT2 convF)) (Cauchy_cont_Lim _ _ _ _ _ (ProjT2 convF)). apply Fun_Series_Sum_char. apply Cauchy_conv_fun_seq'. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series