proposition: Lemma Diffble_Sumx : forall n f, ext_fun_seq' f -> (forall i Hi, Diffble I pI (f i Hi)) -> Diffble I pI (FSumx n f).
proof: Proof. intros n f Hgood hypF. split. red in |- *; intros. apply FSumx_pred'; auto. intros. elim (hypF i Hi); auto. intros; apply Diffble_I_Sumx. intros i Hi; elim (hypF i Hi); auto. Qed.
imports: CoRN.ftc.MoreIntervals