proposition: Lemma Continuous_I_Sumx : forall n (f : forall i, i < n -> PartIR), (forall i Hi, Continuous_I Hab (f i Hi)) -> Continuous_I Hab (FSumx n f).
proof: Proof. intro; induction n as [| n Hrecn]; intros f contF. simpl in |- *; apply Continuous_I_const. simpl in |- *; apply Continuous_I_plus. apply Hrecn. intros; apply contF. apply contF. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac