proposition: Lemma fun_Lim_seq_mult : forall H H', conv_fun_seq' a b Hab (fun n => f n{*}g n) (Cauchy_fun_seq_Lim _ _ _ _ _ Hf{*}Cauchy_fun_seq_Lim _ _ _ _ _ Hg) H H'.
proof: Proof. intros. set (F := Cauchy_fun_seq_Lim _ _ _ _ _ Hf) in *. cut (Continuous_I Hab F); [ intro H0 | unfold F in |- *; Contin ]. cut (conv_fun_seq' _ _ _ _ _ contf H0). 2: unfold F in |- *; apply Cauchy_conv_fun_seq'; assumption. intro convF. set (G := Cauchy_fun_seq_Lim _ _ _ _ _ Hg) in *. cut (Continuous_I Hab G); [ intro H1 | unfold G in |- *; Contin ]. cut (conv_fun_seq' _ _ _ _ _ contg H1). 2: unfold G in |- *; apply Cauchy_conv_fun_seq'; assumption. intro convG. cut (Continuous_I Hab F); [ intro HF' | unfold F, I in |- *; apply Cauchy_cont_Lim; assumption ]. cut (Continuous_I Hab G); [ intro HG' | unfold G, I in |- *; apply Cauchy_cont_Lim; assumption ]. apply fun_Lim_seq_mult' with contf contg H0 H1; auto. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval