proposition: Lemma FSeries_Sum_char : forall a b Hab (Hinc : included (Compact Hab) J), Feq (Compact Hab) FSeries_Sum (Fun_Series_Sum (H a b Hab Hinc)).
proof: Proof. intros; FEQ. simpl in |- *; Included. simpl in |- *; unfold h in |- *. apply series_sum_wd; intros; algebra. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions