proposition: Lemma fun_series_convergent_wd_IR : (forall n, Feq J (f n) (g n)) -> fun_series_convergent_IR J f -> fun_series_convergent_IR J g.
proof: Proof. intros. red in |- *; intros. apply fun_series_convergent_wd with f. intros; apply included_Feq with J; auto. auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions