proposition: Lemma Fun_Series_Sum_inv : forall H : fun_series_convergent _ _ Hab (fun n => {--} (f n)), Feq I (Fun_Series_Sum H) {--} (Fun_Series_Sum convF).
proof: Proof. intros. FEQ. try rename X into H0. cut (convergent (fun n : nat => [--] (f n x (contin_imp_inc _ _ _ _ (ProjT1 convF n) x Hx')))). intro H1. simpl in |- *; apply eq_transitive_unfolded with (series_sum _ H1). 2: apply series_sum_inv with (x := fun n : nat => f n x (contin_imp_inc _ _ _ _ (ProjT1 convF n) x Hx')). unfold series_sum in |- *; apply Lim_wd'; intros; simpl in |- *. unfold seq_part_sum in |- *; apply Sum0_wd; intros. rational. apply conv_series_inv with (x := fun n : nat => f n x (contin_imp_inc _ _ _ _ (ProjT1 convF n) x Hx')). apply fun_series_conv_imp_conv with (Hab := Hab) (Hx := fun n : nat => contin_imp_inc _ _ _ _ (ProjT1 convF n) x Hx'); assumption. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series