proposition: Lemma Derivative_FSeries : Derivative J pJ (FSeries_Sum convF) (FSeries_Sum convG).
proof: Proof. apply fun_lim_seq_derivative with (f := fun n : nat => FSum0 n f) (contf := Continuous_Sum0 _ _ (convergent_imp_Continuous _ _ convF)) (contF := Continuous_FSeries_Sum _ _ convF) (g := fun n : nat => FSum0 n g) (contg := Continuous_Sum0 _ _ (convergent_imp_Continuous _ _ convG)) (contG := Continuous_FSeries_Sum _ _ convG). 3: Deriv. apply FSeries_conv. apply FSeries_conv. Qed.
imports: CoRN.ftc.MoreIntegrals CoRN.ftc.CalculusTheorems