proposition: Lemma fun_Lim_seq_mult'_IR : forall H H', conv_fun_seq'_IR J (fun n => f n{*}g n) (F{*}G) H H'.
proof: Proof. intros. red in |- *; intros. eapply fun_Lim_seq_mult'. apply (convF a b Hab Hinc). apply (convG a b Hab Hinc). Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions