proposition: Lemma conv_fun_series_comp : fun_series_convergent _ _ Hab (fun n => g n[o]F).
proof: Proof. destruct convG as [contg X]. assert (incg := fun (n : nat) => contin_imp_inc _ _ _ _ (contg n)). assert (incpsg : forall n : nat, included (Compact Hcd) (Dom (fun_seq_part_sum g n))). intros n. apply contin_imp_inc. apply fun_seq_part_sum_cont. assumption. assert (convG': forall H, Cauchy_fun_seq _ _ Hcd (fun_seq_part_sum g) H). intros H. eapply Cauchy_fun_seq_wd. intros n; apply Feq_reflexive. apply incpsg. apply X. clear X. assert (X0:forall n, maps_into_compacts F (g n) _ _ Hab _ _ Hcd). intros n. split. apply incg. apply rangeF. set (H' := fun n : nat => Continuous_I_comp _ _ _ _ _ _ _ _ contF (contg n) (X0 n)) in *. exists H'. cut (forall n : nat, Continuous_I Hcd (fun_seq_part_sum g n)); [ intro H0 | Contin ]. cut (forall n : nat, Continuous_I Hab ((fun_seq_part_sum g n)[o]F)); [ intro H1 |intros n; eapply Continuous_I_comp with _ _ Hcd; Contin; split;[apply incpsg|apply rangeF]]. apply Cauchy_fun_seq_wd with (fun n : nat => (fun_seq_part_sum g n)[o]F) H1. intros n. FEQ. apply contin_imp_inc; Contin. simpl. apply Sum0_wd; algebra. pose (G:=(Cauchy_fun_seq_Lim _ _ _ _ _ (convG' H0))). assert (contG:Continuous_I Hcd G). unfold G; Contin. assert (contGF:Continuous_I Hab (G[o]F)). apply Continuous_I_comp with c d Hcd; try assumption. split; try assumption. apply contin_imp_inc. assumption. apply conv_Cauchy_fun_seq' with (G[o]F) contGF. refine (fun_Lim_seq_comp' _ _ Hab _ _ Hcd _ _ (fun n => contF) H0 _ _ _ contF contG _ _ _ _ _). intros _; apply rangeF. apply fun_Lim_seq_const. apply (Cauchy_conv_fun_seq' _ _ _ _ _ (convG' H0)). assumption. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries