proposition: Lemma Diffble_Sum0 : forall f, (forall n, Diffble I pI (f n)) -> forall n, Diffble I pI (FSum0 n f).
proof: Proof. intros f hypF n. split. intros x H n0. elim (hypF n0); intros. exact (a x H). intros; apply Diffble_I_Sum0; auto. intro; elim (hypF n0); auto. Qed.
imports: CoRN.ftc.MoreIntervals