proposition: Lemma Continuous_Sumx : forall n (f : forall i, i < n -> PartIR), (forall i Hi, Continuous I (f i Hi)) -> Continuous I (FSumx n f).
proof: Proof. intro; induction n as [| n Hrecn]; intros f contF. simpl in |- *; Contin. simpl in |- *; Contin. Qed.
imports: CoRN.ftc.MoreIntervals