proposition: Lemma fun_Lim_seq_comp_IR : forall H H', conv_fun_seq'_IR I (fun n => g n[o]f n) (Cauchy_fun_seq_Lim_IR _ _ _ Hg[o]Cauchy_fun_seq_Lim_IR _ _ _ Hf) H H'.
proof: Proof. intros H H'. red; intros. destruct (Hmapf a b Hab Hinc) as [c [d [Hcd [Hcd0 Hcd1]]]]. assert (X:forall n : nat, Continuous_I (a:=a) (b:=b) Hab (g n[o]f n)). intros n. apply Continuous_I_comp with c d Hcd. destruct (contf n) as [A B]. apply B. assumption. destruct (contg n) as [A B]. apply B. assumption. split. destruct (contg n) as [A B]. eapply included_trans. apply Hcd0. assumption. apply Hcd1. assert (W:forall (x : IR) (Hx : Dom (Cauchy_fun_seq_Lim a b Hab f (fun n : nat => included_imp_Continuous I (f n) (contf n) a b Hab Hinc) (Hf a b Hab Hinc)) x), Compact Hab x -> Compact Hcd (Cauchy_fun_seq_Lim a b Hab f (fun n : nat => included_imp_Continuous I (f n) (contf n) a b Hab Hinc) (Hf a b Hab Hinc) x Hx)). intros x Hx Habx. pose (Z:=fun i => contin_imp_inc a b Hab (f i) (included_imp_Continuous I (f i) (contf i) a b Hab Hinc) x Hx). simpl. assert (HcdX := fun n => Hcd1 n x (Z n) Habx). split;[apply leEq_seq_so_leEq_Lim|apply seq_leEq_so_Lim_leEq]; intros i; simpl; destruct (HcdX i); assumption. assert (Z0:Continuous_I (a:=a) (b:=b) Hab (Cauchy_fun_seq_Lim c d Hcd g (fun n : nat => included_imp_Continuous J (g n) (contg n) c d Hcd Hcd0) (Hg c d Hcd Hcd0)[o] Cauchy_fun_seq_Lim a b Hab f (fun n : nat => included_imp_Continuous I (f n) (contf n) a b Hab Hinc) (Hf a b Hab Hinc))). apply Continuous_I_comp with c d Hcd; try apply Cauchy_cont_Lim. split. apply contin_imp_inc. apply Cauchy_cont_Lim. apply W. assert (Z:=fun_Lim_seq_comp _ _ Hab _ _ Hcd _ _ _ _ Hcd1 (Hf _ _ Hab Hinc) (Hg _ _ Hcd Hcd0) X Z0). eapply conv_fun_seq'_wdr;[|apply Z]. clear Z Z0. apply Feq_comp with (Compact Hcd). apply W. intros x Hx Habx. simpl. pose (Z:=fun i => (Continuous_imp_inc I (f i) (contf i) x Hx)). assert (HcdX := fun n => Hcd1 n x (Z n) Habx). split;[apply leEq_seq_so_leEq_Lim|apply seq_leEq_so_Lim_leEq]; intros i; simpl; destruct (HcdX i); assumption. apply Feq_symmetric. apply Cauchy_fun_seq_Lim_char. apply Feq_symmetric. apply Cauchy_fun_seq_Lim_char. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries