proposition: Lemma conv_fun_series_scal : fun_series_convergent _ _ Hab (fun n => H{*}f n).
proof: Proof. elim convF; intros contF convF'. set (H' := fun n : nat => Continuous_I_mult _ _ _ _ _ contH (contF n)) in *; exists H'. cut (forall n : nat, Continuous_I Hab (fun_seq_part_sum f n)); [ intro H0 | Contin ]. cut (forall n : nat, Continuous_I Hab (H{*}fun_seq_part_sum f n)); [ intro H1 | Contin ]. unfold I in |- *; apply Cauchy_fun_seq_wd with (fun n : nat => H{*}fun_seq_part_sum f n) H1. 2: apply fun_Cauchy_prop_mult with (f := fun n : nat => H) (contf := fun n : nat => contH) (g := fun_seq_part_sum f) (contg := H0). intro; FEQ. apply contin_imp_inc; Contin. simpl in |- *. unfold seq_part_sum in |- *. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. 2: apply Sum0_comm_scal' with (s := fun m : nat => f m x (ProjIR2 Hx m)). apply Sum0_wd; intros; rational. apply fun_Cauchy_prop_const. apply Cauchy_fun_seq_wd with (f := fun_seq_part_sum f) (contf := fun_seq_part_sum_cont _ _ _ _ contF). 2: assumption. intro; apply Feq_reflexive; Included. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series