proposition: Lemma conv_fun_series_plus : fun_series_convergent _ _ Hab (fun n => f n{+}g n).
proof: Proof. elim convF; intros contF convF'. elim convG; intros contG convG'. assert (H := fun n : nat => Continuous_I_plus _ _ _ _ _ (contF n) (contG n)); exists H. cut (forall n : nat, Continuous_I Hab (fun_seq_part_sum f n{+}fun_seq_part_sum g n)); [ intro H0 | Contin ]. apply Cauchy_fun_seq_wd with (f := fun n : nat => fun_seq_part_sum f n{+}fun_seq_part_sum g n) (contf := H0). 2: eapply fun_Cauchy_prop_plus; auto; [ apply convF' | apply convG' ]. intros; apply eq_imp_Feq. Included. apply contin_imp_inc; Contin. intros; simpl in |- *. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply Sum0_plus_Sum0. apply Sum0_wd; intros; rational. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series