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