proposition: Lemma Fun_Series_Sum_comp : forall H' : fun_series_convergent _ _ Hab (fun n => g n[o]F), Feq I (Fun_Series_Sum H') (Fun_Series_Sum convG[o]F).
proof: Proof. intros H'. FEQ. simpl. apply series_sum_wd. algebra. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries