proposition: Lemma Fun_Series_Sum_strext : forall x y Hx Hy, series_sum _ (fun_series_conv_imp_conv H x Hx (fun n => incf n x Hx)) [#] series_sum _ (fun_series_conv_imp_conv H y Hy (fun n => incf n y Hy)) -> x [#] y.
proof: Proof. intros x y Hx Hy H0. unfold series_sum in H0. elim (Lim_strext _ _ H0); intros m Hm. simpl in Hm; unfold seq_part_sum in Hm. elim (Sum0_strext _ _ _ _ Hm); intros i H1 H2. exact (pfstrx _ _ _ _ _ _ H2). Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series