proposition: Lemma Derivative_I_Sumx : forall n (f f' : forall i, i < n -> PartIR), (forall i Hi Hi', Derivative_I Hab' (f i Hi) (f' i Hi')) -> Derivative_I Hab' (FSumx n f) (FSumx n f').
proof: Proof. intro; induction n as [| n Hrecn]; intros f f' derF. simpl in |- *; apply Derivative_I_const; auto. simpl in |- *; apply Derivative_I_plus; auto. Qed.
imports: CoRN.ftc.Derivative