proposition: Lemma fun_Lim_seq_comp : forall H H', conv_fun_seq' a b Hab (fun n => g n[o]f n) (Cauchy_fun_seq_Lim _ _ _ _ _ Hg[o]Cauchy_fun_seq_Lim _ _ _ _ _ Hf) H H'.
proof: Proof. intros H H' e H0. set (F := Cauchy_fun_seq_Lim _ _ _ _ _ Hf) in *. cut (Continuous_I Hab F). intro H1. 2: unfold F in |- *; apply Cauchy_cont_Lim. cut (conv_fun_seq' _ _ _ _ _ contf H1). 2: unfold F in |- *; apply Cauchy_conv_fun_seq'; assumption. intro Hf'. set (G := Cauchy_fun_seq_Lim _ _ _ _ _ Hg) in *. cut (Continuous_I Hcd G). intro H2. 2: unfold G in |- *; apply Cauchy_cont_Lim. cut (conv_fun_seq' _ _ _ _ _ contg H2). 2: unfold G in |- *; apply Cauchy_conv_fun_seq'; assumption. intro Hg'. assert (X: (forall (x : IR) (Hx : Dom F x), I x -> Compact Hcd (F x Hx)) ). intros x Hx Hx'. assert (X:=fun_conv_imp_seq_conv _ _ Hab _ contf _ H1 Hf' _ Hx' (fun n => incf n _ Hx') Hx). assert (X0:Cauchy_prop2 (fun n : nat => Part (f n) x ((fun n0 : nat => incf n0 x Hx') n))). exists (F x Hx). assumption. pose (cs:= (Build_CauchySeq _ _ (Cauchy_prop2_prop _ X0))). assert (X1:=Limits_unique cs _ X). apply compact_wd with (Lim cs);[|apply eq_symmetric; assumption]. split;[apply leEq_seq_so_leEq_Lim|apply seq_leEq_so_Lim_leEq]; intros i; simpl; destruct (rangef i _ (incf i _ Hx') Hx'); assumption. apply (fun_Lim_seq_comp' _ _ H1 H2 Hf' Hg' X H); auto. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries