proposition: Lemma is_RInt_fct_extend_snd (f : R -> U * V) (a b : R) (l : U * V) : is_RInt f a b l -> is_RInt (fun t => snd (f t)) a b (snd l).
proof: Proof. intros Hf P [eP HP]. destruct (Hf (fun u : U * V => P (snd u))) as [ef Hf']. exists eP => y Hy. apply HP. apply Hy. exists ef => y H1 H2. replace (Riemann_sum (fun t : R => snd (f t)) y) with (snd (Riemann_sum f y)). by apply Hf'. clear. apply SF_cons_ind with (s := y) => {y} [x0 | [x1 y0] y IH]. by rewrite /Riemann_sum /=. by rewrite ?Riemann_sum_cons /= IH. Qed.
imports: Coq(Reals Psatz) mathcomp(ssreflect ssrbool ssrfun eqtype seq) Markov Rcomplements Rbar Lub Lim_seq SF_seq Continuity Hierarchy