proposition: Lemma Fun_Series_Sum_char' : forall contf H, Feq (Compact Hab) (Fun_Series_Sum convF) (Cauchy_fun_seq_Lim _ _ Hab (fun_seq_part_sum f) contf H).
proof: Proof. intros. FEQ. simpl in |- *; unfold series_sum in |- *. apply Lim_wd'; simpl in |- *; intros. unfold seq_part_sum in |- *; apply Sum0_wd; intros; algebra. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series