proposition: Lemma fun_Lim_seq_comp'_IR : (conv_fun_seq'_IR _ _ _ contf contF) -> (conv_fun_seq'_IR _ _ _ contg contG) -> forall H H', conv_fun_seq'_IR I (fun n => g n[o]f n) (G[o]F) H H'.
proof: Proof. red in |- *; intros. destruct (Hmapf a b Hab Hinc) as [c [d [Hcd [Hcd0 Hcd1]]]]. eapply fun_Lim_seq_comp'. apply Hcd1. apply (X a b Hab Hinc). apply (X0 _ _ Hcd Hcd0). intros. assert (Y:forall n : nat, Dom (f n) x). intros n. refine (Continuous_imp_inc _ _ _ _ _). 1:apply contf. Included. rename H0 into X1. assert (Z:=fun_conv_imp_seq_conv _ _ _ _ _ _ _ (X a b Hab Hinc) x X1 Y Hx). pose (seq:= Build_CauchySeq2_y _ _ Z). assert (Z0:=Limits_unique seq (F x Hx) Z). apply (compact_wd c d Hcd (Lim seq)). assert (HcdX := fun n => Hcd1 n x (Y n) X1). split;[apply leEq_seq_so_leEq_Lim|apply seq_leEq_so_Lim_leEq]; intros i; simpl; destruct (HcdX i); assumption. apply eq_symmetric; assumption. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries