proposition: Lemma Fun_Series_Sum_scal : forall H' : fun_series_convergent _ _ Hab (fun n => H{*}f n), Feq I (Fun_Series_Sum H') (H{*}Fun_Series_Sum convF).
proof: Proof. elim convF; intros contF convF'. intros. unfold I in |- *; FEQ. try rename X into H0. cut (convergent (fun n : nat => Part H x (ProjIR1 Hx') [*] f n x (contin_imp_inc _ _ _ _ (contF n) _ (ProjIR2 Hx')))). intro H1. apply eq_transitive_unfolded with (series_sum (fun n : nat => Part H x (ProjIR1 Hx') [*] f n x (contin_imp_inc _ _ _ _ (contF n) _ (ProjIR2 Hx'))) H1). 2: simpl in |- *; apply series_sum_mult_scal with (x := fun n : nat => f n x (contin_imp_inc _ _ _ _ (contF n) _ (ProjIR2 Hx'))). simpl in |- *; unfold series_sum in |- *. apply Lim_wd'; intros; simpl in |- *. unfold seq_part_sum in |- *; apply Sum0_wd; intros; rational. intros e H1. elim H'; intros H'' 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 Hx). apply AbsIR_wd; simpl in |- *. unfold seq_part_sum in |- *; apply cg_minus_wd; apply Sum0_wd; intros; rational. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series