proposition: Lemma FSeries_Sum_wd' : (forall n, Feq J (f n) (g n)) -> Feq J (FSeries_Sum convF) (FSeries_Sum convG).
proof: Proof. intros H. apply included_Feq'; intros a b Hab H0. eapply Feq_transitive. apply (FSeries_Sum_char _ _ convF a b Hab H0). eapply Feq_transitive. 2: apply Feq_symmetric; apply (FSeries_Sum_char _ _ convG a b Hab H0). apply Fun_Series_Sum_wd'. intro; apply included_Feq with J; auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions