proposition: Lemma fun_seq_part_sum_cont : (forall n, Continuous_I Hab (f n)) -> forall n, Continuous_I Hab (fun_seq_part_sum n).
proof: Proof. intros; unfold fun_seq_part_sum in |- *. Contin. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series