proposition: Lemma Fun_Series_Sum_plus : forall H : fun_series_convergent _ _ Hab (fun n => f n{+}g n), Feq I (Fun_Series_Sum H) (Fun_Series_Sum convF{+}Fun_Series_Sum convG).
proof: Proof. intros. apply eq_imp_Feq. Included. Included. intros x H0 Hx Hx'; simpl in |- *. elim convF; intros contF convF'. elim convG; intros contG convG'. cut (convergent (fun n : nat => Part _ _ (contin_imp_inc _ _ _ _ (contF n) x (ProjIR1 Hx')) [+] Part _ _ (contin_imp_inc _ _ _ _ (contG n) x (ProjIR2 Hx')))). intro H1. eapply eq_transitive_unfolded. 2: apply series_sum_plus with (x := fun n : nat => Part _ _ (contin_imp_inc _ _ _ _ (contF n) x (ProjIR1 Hx'))) (y := fun n : nat => Part _ _ (contin_imp_inc _ _ _ _ (contG n) x (ProjIR2 Hx'))) (H := H1). apply series_sum_wd; intro; rational. intros e H1. elim H; intros cont H'. elim (H' _ H1); intros N HN. exists N; intros. apply AbsIR_imp_AbsSmall. eapply leEq_wdl. apply (HN m N H2 (le_n N) x H0). apply AbsIR_wd; unfold fun_seq_part_sum in |- *. simpl in |- *. unfold seq_part_sum in |- *; apply cg_minus_wd; apply Sum0_wd; intros; rational. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series