proposition: Lemma derivable_pt_lim_sum_f_C0 : forall (An : nat -> C -> C) (Bn : nat -> C -> C), (forall z n, derivable_pt_lim (An n) z (Bn n z)) -> forall z n, derivable_pt_lim (fun z => sum_f_C0 (fun n => An n z) n) z (sum_f_C0 (fun n => Bn n z) n).
proof: Proof. intros An Bn An_deriv z n ; induction n. simpl ; apply An_deriv. simpl ; apply derivable_pt_lim_add ; [apply IHn | apply An_deriv]. Qed.
imports: Cprop_base Ctacfield Cfunctions Cpow Csequence_def Cpser_def Cpser_base_facts Canalysis_def Canalysis_deriv