proposition: Lemma FSeries_conv : forall (convF : fun_series_convergent_IR J f) H H', conv_fun_seq'_IR J (fun n => FSum0 n f) (FSeries_Sum convF) H H'.
proof: Proof. intros. red in |- *; intros. elim (convF _ _ _ Hinc); intros Hcont Hconv. apply conv_fun_seq'_wdr with (f := fun n : nat => FSum0 n f) (contf := fun n : nat => included_imp_Continuous _ _ (H n) _ _ _ Hinc) (contF := Fun_Series_Sum_cont _ _ _ _ (convF _ _ _ Hinc)). apply Feq_symmetric; apply FSeries_Sum_char. apply conv_fun_seq'_wdl with (f := fun_seq_part_sum f) (contf := fun n : nat => included_imp_Continuous _ _ (H n) _ _ _ Hinc) (contF := Fun_Series_Sum_cont _ _ _ _ (convF _ _ _ Hinc)). intro; apply Feq_reflexive. red in |- *; intros. simpl in |- *; intros. apply (contin_imp_inc _ _ _ _ (Hcont n0)); auto. apply fun_series_conv. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions