proposition: Lemma limit_of_integral : conv_fun_seq'_IR J f F contf contF -> forall x y Hxy, included (Compact Hxy) J -> forall Hf HF, Cauchy_Lim_prop2 (fun n => integral x y Hxy (f n) (Hf n)) (integral x y Hxy F HF).
proof: Proof. intros H x y Hxy H0 Hf HF. assert (Hx : J x). apply H0; apply compact_inc_lft. assert (Hy : J y). apply H0; apply compact_inc_rht. set (g := fun n : nat => ( [-S-]contf n) x Hx) in *. set (G := ( [-S-]contF) x Hx) in *. set (Hxg := fun n : nat => Hy) in *. apply Lim_wd with (Part G y Hy). simpl in |- *; apply Integral_integral. apply Cauchy_Lim_prop2_wd with (fun n : nat => Part (g n) y (Hxg n)). 2: intro; simpl in |- *; apply Integral_integral. cut (forall n : nat, Continuous_I Hxy (g n)). intro H1. cut (Continuous_I Hxy G). intro H2. apply fun_conv_imp_seq_conv with (contf := H1) (contF := H2). set (H4 := fun n : nat => included_imp_Continuous _ _ (contf n) _ _ _ H0) in *. set (H5 := included_imp_Continuous _ _ contF _ _ _ H0) in *. unfold g, G in |- *. apply fun_lim_seq_integral with H4 H5. unfold H4, H5 in |- *. apply H; auto. apply compact_inc_lft. apply compact_inc_rht. unfold G in |- *; apply included_imp_Continuous with J; Contin. intro; unfold g in |- *; apply included_imp_Continuous with J; Contin. Qed.
imports: CoRN.ftc.MoreIntegrals CoRN.ftc.CalculusTheorems