diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 23ad671e24..8e5311d49c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -77,6 +77,24 @@
     `powere_posNyr`, `fine_powere_pos`, `powere_pos_ge0`,
     `powere_pos_gt0`, `powere_pos_eq0`, `powere_posM`, `powere12_sqrt`
 
+
+- in file `kernel.v`,
+  + new definitions `kseries`, `measure_fam_uub`, `kzero`, `kdirac`, 
+    `prob_pointed`, `mset`, `pset`, `pprobability`, `kprobability`, `kadd`, 
+    `mnormalize`, `knormalize`, `kcomp`, and `mkcomp`.
+  + new lemmas `eq_kernel`, `measurable_fun_kseries`, `integral_kseries`,
+    `measure_fam_uubP`, `eq_sfkernel`, `kzero_uub`, `sfinite_finite`,
+    `sfinite`, `sfinite_kernel_measure`, `finite_kernel_measure`,
+    `measurable_prod_subset_xsection_kernel`,
+    `measurable_fun_xsection_finite_kernel`,
+    `measurable_fun_xsection_integral`,
+    `measurable_fun_integral_finite_kernel`,
+    `measurable_fun_integral_sfinite_kernel`, `lt0_mset`, `gt1_mset`,
+    `kernel_measurable_eq_cst`, `kernel_measurable_neq_cst`, `kernel_measurable_fun_eq_cst`,
+    `measurable_fun_kcomp_finite`, `mkcomp_sfinite`,
+    `measurable_fun_mkcomp_sfinite`, `measurable_fun_preimage_integral`,
+    `measurable_fun_integral_kernel`, and `integral_kcomp`.
+
 ### Changed
 
 - in `mathcomp_extra.v`
@@ -89,6 +107,8 @@
     `power_pos_inv`, `power_pos_intmul`
 - in `lebesgue_measure.v`:
   + lemmas `measurable_fun_ln`, `measurable_fun_power_pos`
+- in `lebesgue_integral.v`:
+  + lemma `xsection_ndseq_closed` generalized from a measure to a family of measures
 
 ### Changed
 
diff --git a/_CoqProject b/_CoqProject
index 594eaceef7..8af2f54b32 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,6 +39,7 @@ theories/lebesgue_integral.v
 theories/summability.v
 theories/signed.v
 theories/itv.v
+theories/kernel.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v
diff --git a/theories/kernel.v b/theories/kernel.v
new file mode 100644
index 0000000000..36cc91f472
--- /dev/null
+++ b/theories/kernel.v
@@ -0,0 +1,1137 @@
+(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
+Require Import mathcomp_extra boolp classical_sets signed functions cardinality.
+Require Import reals ereal topology normedtype sequences esum measure.
+Require Import lebesgue_measure fsbigop numfun lebesgue_integral.
+
+(******************************************************************************)
+(*                                  Kernels                                   *)
+(*                                                                            *)
+(* This file provides a formation of kernels and extends the theory of        *)
+(* measures with, e.g., Tonelli-Fubini's theorem for s-finite measures.       *)
+(* The main result is the fact that s-finite kernels are stable by            *)
+(* composition.                                                               *)
+(*                                                                            *)
+(*   finite_measure mu == the measure mu is finite                            *)
+(*  sfinite_measure mu == the measure mu is s-finite                          *)
+(*       R.-ker X ~> Y == kernel                                              *)
+(*             kseries == countable sum of kernels                            *)
+(*     R.-sfker X ~> Y == s-finite kernel                                     *)
+(*      R.-fker X ~> Y == finite kernel                                       *)
+(*     R.-spker X ~> Y == subprobability kernel                               *)
+(*      R.-pker X ~> Y == probability kernel                                  *)
+(*            mset U r == the set probability measures mu such that mu U < r  *)
+(*                pset == the sets mset U r with U measurable and r \in [0,1] *)
+(*        pprobability == the measurable type generated by pset               *)
+(*      kprobability m == kernel defined by a probability measure             *)
+(*           kdirac mf == kernel defined by a measurable function             *)
+(*          kadd k1 k2 == lifting of the addition of measures to kernels      *)
+(*        mnormalize f == normalization of a kernel to a probability          *)
+(*              l \; k == composition of kernels                              *)
+(*                                                                            *)
+(* ref: R. Affeldt, C. Cohen, A. Saito, Semantics of probabilistic programs   *)
+(* using s-finite kernels in Coq. CPP 2023                                    *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+Import numFieldTopology.Exports.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+Local Open Scope ereal_scope.
+
+Reserved Notation "R .-ker X ~> Y"
+  (at level 42, format "R .-ker  X  ~>  Y").
+Reserved Notation "R .-sfker X ~> Y"
+  (at level 42, format "R .-sfker  X  ~>  Y").
+Reserved Notation "R .-fker X ~> Y"
+  (at level 42, format "R .-fker  X  ~>  Y").
+Reserved Notation "R .-spker X ~> Y"
+  (at level 42, format "R .-spker  X  ~>  Y").
+Reserved Notation "R .-pker X ~> Y"
+  (at level 42, format "R .-pker  X  ~>  Y").
+
+HB.mixin Record isKernel d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) (k : X -> {measure set Y -> \bar R}) :=
+  {measurable_kernel : forall U, measurable U -> measurable_fun setT (k ^~ U)}.
+
+#[short(type=kernel)]
+HB.structure Definition Kernel
+    d d' (X : measurableType d) (Y : measurableType d') (R : realType) :=
+  { k & isKernel _ _ X Y R k }.
+Notation "R .-ker X ~> Y" := (kernel X Y R).
+
+Arguments measurable_kernel {_ _ _ _ _} _.
+
+Lemma kernel_measurable_eq_cst d d' (T : measurableType d)
+    (T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k :
+  measurable [set t | f t setT == k].
+Proof.
+rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set k]); last first.
+  by apply/seteqP; split => t/= /eqP.
+have /(_ measurableT [set k]) := measurable_kernel f setT measurableT.
+by rewrite setTI; exact.
+Qed.
+
+Lemma kernel_measurable_neq_cst d d' (T : measurableType d)
+    (T' : measurableType d') (R : realType)  (f : R.-ker T ~> T') k :
+  measurable [set t | f t setT != k].
+Proof.
+rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set~ k]); last first.
+  by apply/seteqP; split => t /eqP.
+have /(_ measurableT [set~ k]) := measurable_kernel f setT measurableT.
+by rewrite setTI; apply => //; exact: measurableC.
+Qed.
+
+Lemma kernel_measurable_fun_eq_cst d d' (T : measurableType d)
+    (T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k :
+  measurable_fun setT (fun t => f t setT == k).
+Proof.
+move=> _ /= B mB; rewrite setTI.
+have [/eqP->|/eqP->|/eqP->|/eqP->] := set_bool B.
+- exact: kernel_measurable_eq_cst.
+- rewrite (_ : _ @^-1` _ = [set b | f b setT != k]); last first.
+    by apply/seteqP; split => [t /negbT//|t /negbTE].
+  exact: kernel_measurable_neq_cst.
+- by rewrite preimage_set0.
+- by rewrite preimage_setT.
+Qed.
+
+Lemma eq_kernel d d' (T : measurableType d) (T' : measurableType d')
+    (R : realType) (k1 k2 : R.-ker T ~> T') :
+  (forall x U, k1 x U = k2 x U) -> k1 = k2.
+Proof.
+move: k1 k2 => [m1 [[?]]] [m2 [[?]]] /= k12.
+have ? : m1 = m2.
+  by apply/funext => t; apply/eq_measure; apply/funext => U; rewrite k12.
+by subst m1; f_equal; f_equal; f_equal; apply/Prop_irrelevance.
+Qed.
+
+Section kseries.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variable k : (R.-ker X ~> Y)^nat.
+
+Definition kseries : X -> {measure set Y -> \bar R} :=
+  fun x => [the measure _ _ of mseries (k ^~ x) 0].
+
+Lemma measurable_fun_kseries (U : set Y) :
+  measurable U ->
+  measurable_fun setT (kseries ^~ U).
+Proof.
+move=> mU.
+by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel.
+Qed.
+
+HB.instance Definition _ :=
+  isKernel.Build _ _ _ _ _ kseries measurable_fun_kseries.
+
+End kseries.
+
+Lemma integral_kseries d d' (X : measurableType d) (Y : measurableType d')
+  (R : realType) (k : (R.-ker X ~> Y)^nat) (f : Y -> \bar R) x :
+  (forall y, 0 <= f y) ->
+  measurable_fun setT f ->
+  \int[kseries k x]_y (f y) = \sum_(i <oo) \int[k i x]_y (f y).
+Proof.
+by move=> f0 mf; rewrite /kseries/= ge0_integral_measure_series.
+Qed.
+
+Section measure_fam_uub.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : numFieldType).
+Variable k : X -> {measure set Y -> \bar R}.
+
+Definition measure_fam_uub := exists r, forall x, k x [set: Y] < r%:E.
+
+Lemma measure_fam_uubP : measure_fam_uub <->
+  exists r : {posnum R}, forall x, k x [set: Y] < r%:num%:E.
+Proof.
+split => [|] [r kr]; last by exists r%:num.
+suff r_gt0 : (0 < r)%R by exists (PosNum r_gt0).
+by rewrite -lte_fin; apply: (le_lt_trans _ (kr point)).
+Qed.
+
+End measure_fam_uub.
+
+HB.mixin Record Kernel_isSFinite_subdef
+    d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) (k : X -> {measure set Y -> \bar R}) := {
+  sfinite_subdef : exists2 s : (R.-ker X ~> Y)^nat,
+    forall n, measure_fam_uub (s n) &
+    forall x U, measurable U -> k x U = kseries s x U }.
+
+#[short(type=sfinite_kernel)]
+HB.structure Definition SFiniteKernel
+    d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) :=
+  {k of @Kernel _ _ _ _ R k & Kernel_isSFinite_subdef _ _ X Y R k }.
+Notation "R .-sfker X ~> Y" := (sfinite_kernel X Y R).
+
+Arguments sfinite_subdef {_ _ _ _ _} _.
+
+Lemma eq_sfkernel d d' (T : measurableType d) (T' : measurableType d')
+    (R : realType) (k1 k2 : R.-sfker T ~> T') :
+  (forall x U, k1 x U = k2 x U) -> k1 = k2.
+Proof.
+move: k1 k2 => [m1 [[?] [?]]] [m2 [[?] [?]]] /= k12.
+have ? : m1 = m2.
+  by apply/funext => t; apply/eq_measure; apply/funext => U; rewrite k12.
+by subst m1; f_equal; f_equal; f_equal; apply/Prop_irrelevance.
+Qed.
+
+HB.mixin Record SFiniteKernel_isFinite
+    d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) (k : X -> {measure set Y -> \bar R}) :=
+  { measure_uub : measure_fam_uub k }.
+
+#[short(type=finite_kernel)]
+HB.structure Definition FiniteKernel
+    d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) :=
+  {k of @SFiniteKernel _ _ _ _ _ k &
+        SFiniteKernel_isFinite _ _ X Y R k }.
+Notation "R .-fker X ~> Y" := (finite_kernel X Y R).
+
+Arguments measure_uub {_ _ _ _ _} _.
+
+HB.factory Record Kernel_isFinite d d' (X : measurableType d)
+    (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R})
+    of isKernel _ _ _ _ _ k := {
+  measure_uub : measure_fam_uub k }.
+
+Section kzero.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+
+Definition kzero : X -> {measure set Y -> \bar R} :=
+  fun _ : X => [the measure _ _ of mzero].
+
+Let measurable_fun_kzero U : measurable U ->
+  measurable_fun setT (kzero ^~ U).
+Proof. by move=> ?/=; exact: measurable_fun_cst. Qed.
+
+HB.instance Definition _ :=
+  @isKernel.Build _ _ X Y R kzero measurable_fun_kzero.
+
+Lemma kzero_uub : measure_fam_uub kzero.
+Proof. by exists 1%R => /= t; rewrite /mzero/=. Qed.
+
+End kzero.
+
+HB.builders Context d d' (X : measurableType d) (Y : measurableType d')
+  (R : realType) k of Kernel_isFinite d d' X Y R k.
+
+Lemma sfinite_finite :
+  exists2 k_ : (R.-ker _ ~> _)^nat, forall n, measure_fam_uub (k_ n) &
+    forall x U, measurable U -> k x U = mseries (k_ ^~ x) 0 U.
+Proof.
+exists (fun n => if n is O then [the _.-ker _ ~> _ of k] else
+  [the _.-ker _ ~> _ of @kzero _ _ X Y R]).
+  by case => [|_]; [exact: measure_uub|exact: kzero_uub].
+move=> t U mU/=; rewrite /mseries.
+rewrite (nneseries_split 1%N)// big_ord_recl/= big_ord0 adde0.
+rewrite ereal_series (@eq_eseriesr _ _ (fun=> 0%E)); last by case.
+by rewrite eseries0// adde0.
+Qed.
+
+HB.instance Definition _ :=
+  @Kernel_isSFinite_subdef.Build d d' X Y R k sfinite_finite.
+
+HB.instance Definition _ :=
+  @SFiniteKernel_isFinite.Build  d d' X Y R k measure_uub.
+
+HB.end.
+
+Section sfinite.
+Context d d' (X : measurableType d) (Y : measurableType d').
+Variables (R : realType) (k : R.-sfker X ~> Y).
+
+Let s : (X -> {measure set Y -> \bar R})^nat :=
+  let: exist2 x _ _ := cid2 (sfinite_subdef k) in x.
+
+Let ms n : @isKernel d d' X Y R (s n).
+Proof.
+split; rewrite /s; case: cid2 => /= s' s'_uub kE.
+exact: measurable_kernel.
+Qed.
+
+HB.instance Definition _ n := ms n.
+
+Let s_uub n : measure_fam_uub (s n).
+Proof. by rewrite /s; case: cid2. Qed.
+
+HB.instance Definition _ n :=
+  @Kernel_isFinite.Build d d' X Y R (s n) (s_uub n).
+
+Lemma sfinite : exists s : (R.-fker X ~> Y)^nat,
+  forall x U, measurable U -> k x U = kseries s x U.
+Proof.
+exists (fun n => [the _.-fker _ ~> _ of s n]) => x U mU.
+by rewrite /s /= /s; by case: cid2 => ? ? ->.
+Qed.
+
+End sfinite.
+
+Lemma sfinite_kernel_measure d d' (Z : measurableType d) (X : measurableType d')
+    (R : realType) (k : R.-sfker Z ~> X) (z : Z) :
+  sfinite_measure (k z).
+Proof.
+have [s ks] := sfinite k.
+exists (s ^~ z).
+  move=> n; have [r snr] := measure_uub (s n).
+  by apply: lty_fin_num_fun; rewrite (lt_le_trans (snr _))// leey.
+by move=> U mU; rewrite ks.
+Qed.
+
+HB.instance Definition _ d d' (X : measurableType d)
+    (Y : measurableType d') (R : realType) :=
+  @Kernel_isFinite.Build _ _ _ _ R (@kzero _ _ X Y R)
+                                   (@kzero_uub _ _ X Y R).
+
+HB.factory Record Kernel_isSFinite d d' (X : measurableType d)
+    (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R})
+    of isKernel _ _ _ _ _ k := {
+  sfinite : exists s : (R.-fker X ~> Y)^nat,
+    forall x U, measurable U -> k x U = kseries s x U }.
+
+HB.builders Context d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) k of Kernel_isSFinite d d' X Y R k.
+
+Lemma sfinite_subdef : Kernel_isSFinite_subdef d d' X Y R k.
+Proof.
+split; have [s sE] := sfinite; exists s => //.
+by move=> n; exact: measure_uub.
+Qed.
+
+HB.instance Definition _ := (*@isSFinite0.Build d d' X Y R k*) sfinite_subdef.
+
+HB.end.
+
+HB.mixin Record FiniteKernel_isSubProbability
+    d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) (k : X -> {measure set Y -> \bar R}) :=
+  { sprob_kernel : ereal_sup [set k x [set: Y] | x in setT] <= 1}.
+
+#[short(type=sprobability_kernel)]
+HB.structure Definition SubProbabilityKernel
+    d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) :=
+  {k of @FiniteKernel _ _ _ _ _ k &
+        FiniteKernel_isSubProbability _ _ X Y R k }.
+Notation "R .-spker X ~> Y" := (sprobability_kernel X Y R).
+
+HB.factory Record Kernel_isSubProbability
+    d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k
+  := { sprob_kernel : ereal_sup [set k x [set: Y] | x in setT] <= 1}.
+
+HB.builders Context d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) k of Kernel_isSubProbability d d' X Y R k.
+
+Let finite : @Kernel_isFinite d d' X Y R k.
+Proof.
+split; exists 2%R => /= ?; rewrite (@le_lt_trans _ _ 1%:E) ?lte_fin ?ltr1n//.
+by rewrite (le_trans _ sprob_kernel)//; exact: ereal_sup_ub.
+Qed.
+
+HB.instance Definition _ := finite.
+
+HB.instance Definition _ :=
+  @FiniteKernel_isSubProbability.Build _ _ _ _ _ k sprob_kernel.
+
+HB.end.
+
+HB.mixin Record SubProbability_isProbability
+    d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) (k : X -> {measure set Y -> \bar R}) :=
+  { prob_kernel : forall x, k x [set: Y] = 1}.
+
+#[short(type=probability_kernel)]
+HB.structure Definition ProbabilityKernel
+    d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) :=
+  {k of @SubProbabilityKernel _ _ _ _ _ k &
+        SubProbability_isProbability _ _ X Y R k }.
+Notation "R .-pker X ~> Y" := (probability_kernel X Y R).
+
+HB.factory Record Kernel_isProbability
+    d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k
+  := { prob_kernel : forall x, k x setT = 1 }.
+
+HB.builders Context d d' (X : measurableType d) (Y : measurableType d')
+    (R : realType) k of Kernel_isProbability d d' X Y R k.
+
+Let sprob_kernel : @Kernel_isSubProbability d d' X Y R k.
+Proof.
+by split; apply: ub_ereal_sup => x [y _ <-{x}]; rewrite prob_kernel.
+Qed.
+
+HB.instance Definition _ := sprob_kernel.
+
+HB.instance Definition _ :=
+  @SubProbability_isProbability.Build _ _ _ _ _ k prob_kernel.
+
+HB.end.
+
+Lemma finite_kernel_measure d d' (X : measurableType d)
+    (Y : measurableType d') (R : realType) (k : R.-fker X ~> Y) (x : X) :
+  fin_num_fun (k x).
+Proof.
+have [r k_r] := measure_uub k.
+by apply: lty_fin_num_fun; rewrite (@lt_trans _ _ r%:E) ?ltey.
+Qed.
+
+(* see measurable_prod_subset in lebesgue_integral.v;
+   the differences between the two are:
+   - m2 is a kernel instead of a measure (the proof uses the
+     measurability of each measure of the family)
+   - as a consequence, m2D_bounded holds for all x *)
+Section measurable_prod_subset_kernel.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Implicit Types A : set (X * Y).
+
+Section xsection_kernel.
+Variable (k : R.-ker X ~> Y) (D : set Y) (mD : measurable D).
+Let kD x := mrestr (k x) mD.
+HB.instance Definition _ x := Measure.on (kD x).
+Let phi A := fun x => kD x (xsection A x).
+Let XY := [set A | measurable A /\ measurable_fun setT (phi A)].
+
+Let phiM (A : set X) B : phi (A `*` B) = (fun x => kD x B * (\1_A x)%:E).
+Proof.
+rewrite funeqE => x; rewrite indicE /phi/=.
+have [xA|xA] := boolP (x \in A); first by rewrite mule1 in_xsectionM.
+by rewrite mule0 notin_xsectionM// set0I measure0.
+Qed.
+
+Lemma measurable_prod_subset_xsection_kernel :
+    (forall x, exists M, forall X, measurable X -> kD x X < M%:E) ->
+  measurable `<=` XY.
+Proof.
+move=> kD_ub; rewrite measurable_prod_measurableType.
+set C := [set A `*` B | A in measurable & B in measurable].
+have CI : setI_closed C.
+  move=> _ _ [X1 mX1 [X2 mX2 <-]] [Y1 mY1 [Y2 mY2 <-]].
+  exists (X1 `&` Y1); first exact: measurableI.
+  by exists (X2 `&` Y2); [exact: measurableI|rewrite setMI].
+have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT.
+have CXY : C `<=` XY.
+  move=> _ [A mA [B mB <-]]; split; first exact: measurableM.
+  rewrite phiM.
+  apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI.
+  by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA).
+suff monoB : monotone_class setT XY by exact: monotone_class_subset.
+split => //; [exact: CXY| |exact: xsection_ndseq_closed].
+move=> A B BA [mA mphiA] [mB mphiB]; split; first exact: measurableD.
+suff : phi (A `\` B) = (fun x => phi A x - phi B x).
+  by move=> ->; exact: emeasurable_funB.
+rewrite funeqE => x; rewrite /phi/= xsectionD// measureD.
+- by rewrite setIidr//; exact: le_xsection.
+- exact: measurable_xsection.
+- exact: measurable_xsection.
+- have [M kM] := kD_ub x.
+  rewrite (lt_le_trans (kM (xsection A x) _)) ?leey//.
+  exact: measurable_xsection.
+Qed.
+
+End xsection_kernel.
+
+End measurable_prod_subset_kernel.
+
+(* see measurable_fun_xsection in lebesgue_integral.v
+   the difference is that this section uses a finite kernel m2
+   instead of a sigma-finite measure m2 *)
+Section measurable_fun_xsection_finite_kernel.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variable k : R.-fker X ~> Y.
+Implicit Types A : set (X * Y).
+
+Let phi A := fun x => k x (xsection A x).
+Let XY := [set A | measurable A /\ measurable_fun setT (phi A)].
+
+Lemma measurable_fun_xsection_finite_kernel A :
+  A \in measurable -> measurable_fun setT (phi A).
+Proof.
+move: A; suff : measurable `<=` XY by move=> + A; rewrite inE => /[apply] -[].
+move=> /= A mA; rewrite /XY/=; split => //; rewrite (_ : phi _ =
+    (fun x => mrestr (k x) measurableT (xsection A x))); last first.
+  by apply/funext => x//=; rewrite /mrestr setIT.
+apply measurable_prod_subset_xsection_kernel => // x.
+have [r hr] := measure_uub k; exists r => B mB.
+by rewrite (le_lt_trans _ (hr x)) // /mrestr /= setIT le_measure// inE.
+Qed.
+
+End measurable_fun_xsection_finite_kernel.
+
+Section measurable_fun_integral_finite_sfinite.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variable k : X * Y -> \bar R.
+
+Lemma measurable_fun_xsection_integral
+    (l : X -> {measure set Y -> \bar R})
+    (k_ : ({nnsfun [the measurableType _ of (X * Y)%type] >-> R})^nat)
+    (ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat))
+    (k_k : forall z, EFin \o (k_ ^~ z) --> k z) :
+  (forall n r,
+    measurable_fun setT (fun x => l x (xsection (k_ n @^-1` [set r]) x))) ->
+  measurable_fun setT (fun x => \int[l x]_y k (x, y)).
+Proof.
+move=> h.
+rewrite (_ : (fun x => _) =
+    (fun x => lim_esup (fun n => \int[l x]_y (k_ n (x, y))%:E))); last first.
+  apply/funext => x.
+  transitivity (lim (fun n => \int[l x]_y (k_ n (x, y))%:E)); last first.
+    rewrite is_cvg_lim_esupE//.
+    apply: ereal_nondecreasing_is_cvg => m n mn.
+    apply: ge0_le_integral => //.
+    - by move=> y _; rewrite lee_fin.
+    - exact/EFin_measurable_fun/measurable_fun_prod1.
+    - by move=> y _; rewrite lee_fin.
+    - exact/EFin_measurable_fun/measurable_fun_prod1.
+    - by move=> y _; rewrite lee_fin; exact/lefP/ndk_.
+  rewrite -monotone_convergence//.
+  - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: k_k.
+  - by move=> n; exact/EFin_measurable_fun/measurable_fun_prod1.
+  - by move=> n y _; rewrite lee_fin.
+  - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_.
+apply: measurable_fun_lim_esup => n.
+rewrite [X in measurable_fun _ X](_ : _ = (fun x => \int[l x]_y
+    (\sum_(r \in range (k_ n))
+      r * \1_(k_ n @^-1` [set r]) (x, y))%:E)); last first.
+  by apply/funext => x; apply: eq_integral => y _; rewrite fimfunE.
+rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n))
+    (\int[l x]_y (r * \1_(k_ n @^-1` [set r]) (x, y))%:E))); last first.
+  apply/funext => x; rewrite -ge0_integral_fsum//.
+  - by apply: eq_integral => y _; rewrite -fsumEFin.
+  - move=> r.
+    apply/EFin_measurable_fun/measurable_funrM/measurable_fun_prod1 => /=.
+    rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) (measurable_set1 r)))//.
+    exact/measurable_funP.
+  - by move=> m y _; rewrite nnfun_muleindic_ge0.
+apply: emeasurable_fun_fsum => // r.
+rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E *
+    \int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E)); last first.
+  apply/funext => x; under eq_integral do rewrite EFinM.
+  have [r0|r0] := leP 0%R r.
+    rewrite ge0_integralM//; last by move=> y _; rewrite lee_fin.
+    apply/EFin_measurable_fun/measurable_fun_prod1 => /=.
+    rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) (measurable_set1 r)))//.
+    exact/measurable_funP.
+  rewrite integral0_eq; last first.
+    by move=> y _; rewrite preimage_nnfun0// indic0 mule0.
+  by rewrite integral0_eq ?mule0// => y _; rewrite preimage_nnfun0// indic0.
+apply/measurable_funeM.
+rewrite (_ : (fun x => _) = (fun x => l x (xsection (k_ n @^-1` [set r]) x))).
+  exact/h.
+apply/funext => x; rewrite integral_indic//; last first.
+  rewrite (_ : (fun x => _) = xsection (k_ n @^-1` [set r]) x).
+    exact: measurable_xsection.
+  by rewrite /xsection; apply/seteqP; split=> y/= /[!inE].
+congr (l x _); apply/funext => y1/=; rewrite /xsection/= inE.
+by apply/propext; tauto.
+Qed.
+
+Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y)
+    (k0 : forall z, 0 <= k z) (mk : measurable_fun setT k) :
+  measurable_fun setT (fun x => \int[l x]_y k (x, y)).
+Proof.
+have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x).
+apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r.
+have [l_ hl_] := measure_uub l.
+by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
+Qed.
+
+Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y)
+    (k0 : forall t, 0 <= k t) (mk : measurable_fun setT k) :
+  measurable_fun setT (fun x => \int[l x]_y k (x, y)).
+Proof.
+have [k_ [ndk_ k_k]] := approximation measurableT mk (fun xy _ => k0 xy).
+apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r.
+have [l_ hl_] := sfinite l.
+rewrite (_ : (fun x => _) = (fun x =>
+    mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first.
+  by apply/funext => x; rewrite hl_//; exact/measurable_xsection.
+apply: ge0_emeasurable_fun_sum => // m.
+by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
+Qed.
+
+End measurable_fun_integral_finite_sfinite.
+Arguments measurable_fun_xsection_integral {_ _ _ _ _} k l.
+Arguments measurable_fun_integral_finite_kernel {_ _ _ _ _} k l.
+Arguments measurable_fun_integral_sfinite_kernel {_ _ _ _ _} k l.
+
+Section kdirac.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variable f : X -> Y.
+
+Definition kdirac (mf : measurable_fun setT f)
+    : X -> {measure set Y -> \bar R} :=
+  fun x => [the measure _ _ of dirac (f x)].
+
+Hypothesis mf : measurable_fun setT f.
+
+Let measurable_fun_kdirac U : measurable U ->
+  measurable_fun setT (kdirac mf ^~ U).
+Proof.
+move=> mU; apply/EFin_measurable_fun.
+by rewrite (_ : (fun x => _) = mindic R mU \o f)//; exact/measurable_funT_comp.
+Qed.
+
+HB.instance Definition _ := isKernel.Build _ _ _ _ _ (kdirac mf)
+  measurable_fun_kdirac.
+
+Let kdirac_prob x : kdirac mf x setT = 1.
+Proof. by rewrite /kdirac/= diracT. Qed.
+
+HB.instance Definition _ := Kernel_isProbability.Build _ _ _ _ _
+  (kdirac mf) kdirac_prob.
+
+End kdirac.
+Arguments kdirac {d d' X Y R f}.
+
+Section dist_salgebra_instance.
+Context d (T : measurableType d) (R : realType).
+
+Let p0 : probability T R := [the probability _ _ of dirac point].
+
+Definition prob_pointed := Pointed.Class
+  (Choice.Class gen_eqMixin (Choice.Class gen_eqMixin gen_choiceMixin)) p0.
+
+Canonical probability_eqType := EqType (probability T R) prob_pointed.
+Canonical probability_choiceType := ChoiceType (probability T R) prob_pointed.
+Canonical probability_ptType := PointedType (probability T R) prob_pointed.
+
+Definition mset (U : set T) (r : R) := [set mu : probability T R | mu U < r%:E].
+
+Lemma lt0_mset (U : set T) (r : R) : (r < 0)%R -> mset U r = set0.
+Proof.
+move=> r0; apply/seteqP; split => // x/=.
+by apply/negP; rewrite -leNgt (@le_trans _ _ 0)// lee_fin ltW.
+Qed.
+
+Lemma gt1_mset (U : set T) (r : R) :
+  measurable U -> (1 < r)%R -> mset U r = setT.
+Proof.
+move=> mU r1; apply/seteqP; split => // x/= _.
+by rewrite /mset/= (le_lt_trans (probability_le1 _ _)).
+Qed.
+
+Definition pset : set (set (probability T R)) :=
+  [set mset U r | r in `[0%R,1%R] & U in measurable].
+
+Definition pprobability : measurableType pset.-sigma :=
+  [the measurableType _ of salgebraType pset].
+
+End dist_salgebra_instance.
+
+Section kprobability.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variable P : X -> pprobability Y R.
+
+Definition kprobability (mP : measurable_fun setT P)
+  : X -> {measure set Y -> \bar R} := P.
+
+Hypothesis mP : measurable_fun setT P.
+
+Let measurable_fun_kprobability U : measurable U ->
+  measurable_fun setT (kprobability mP ^~ U).
+Proof.
+move=> mU.
+apply: (measurability (ErealGenInftyO.measurableE R)) => _ /= -[_ [r ->] <-].
+rewrite setTI preimage_itv_infty_o -/(P @^-1` mset U r).
+have [r0|r0] := leP 0%R r; last by rewrite lt0_mset// preimage_set0.
+have [r1|r1] := leP r 1%R; last by rewrite gt1_mset// preimage_setT.
+move: mP => /(_ measurableT (mset U r)); rewrite setTI; apply.
+by apply: sub_sigma_algebra; exists r => /=; [rewrite in_itv/= r0|exists U].
+Qed.
+
+HB.instance Definition _ :=
+  @isKernel.Build _ _ X Y R (kprobability mP) measurable_fun_kprobability.
+
+Let kprobability_prob x : kprobability mP x setT = 1.
+Proof. by rewrite /kprobability/= probability_setT. Qed.
+
+HB.instance Definition _ :=
+  @Kernel_isProbability.Build _ _ X Y R (kprobability mP) kprobability_prob.
+
+End kprobability.
+
+Section kadd.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variables k1 k2 : R.-ker X ~> Y.
+
+Definition kadd : X -> {measure set Y -> \bar R} :=
+  fun x => [the measure _ _ of measure_add (k1 x) (k2 x)].
+
+Let measurable_fun_kadd U : measurable U ->
+  measurable_fun setT (kadd ^~ U).
+Proof.
+move=> mU; rewrite /kadd.
+rewrite (_ : (fun _ => _) = (fun x => k1 x U + k2 x U)); last first.
+  by apply/funext => x; rewrite -measure_addE.
+by apply: emeasurable_funD; exact/measurable_kernel.
+Qed.
+
+HB.instance Definition _ :=
+  @isKernel.Build _ _ _ _ _ kadd measurable_fun_kadd.
+End kadd.
+
+Section sfkadd.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variables k1 k2 : R.-sfker X ~> Y.
+
+Let sfinite_kadd : exists2 k_ : (R.-ker _ ~> _)^nat,
+  forall n, measure_fam_uub (k_ n) &
+  forall x U, measurable U ->
+    kadd k1 k2 x U = mseries (k_ ^~ x) 0 U.
+Proof.
+have [f1 hk1] := sfinite k1; have [f2 hk2] := sfinite k2.
+exists (fun n => [the _.-ker _ ~> _ of kadd (f1 n) (f2 n)]).
+  move=> n.
+  have [r1 f1r1] := measure_uub (f1 n).
+  have [r2 f2r2] := measure_uub (f2 n).
+  exists (r1 + r2)%R => x/=.
+  by rewrite /msum !big_ord_recr/= big_ord0 add0e EFinD lte_add.
+move=> x U mU.
+rewrite /kadd/= -/(measure_add (k1 x) (k2 x)) measure_addE hk1//= hk2//=.
+rewrite /mseries -nneseriesD//; apply: eq_eseriesr => n _ /=.
+by rewrite -/(measure_add (f1 n x) (f2 n x)) measure_addE.
+Qed.
+
+HB.instance Definition _ t :=
+  Kernel_isSFinite_subdef.Build _ _ _ _ R (kadd k1 k2) sfinite_kadd.
+End sfkadd.
+
+Section fkadd.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variables k1 k2 : R.-fker X ~> Y.
+
+Let kadd_finite_uub : measure_fam_uub (kadd k1 k2).
+Proof.
+have [f1 hk1] := measure_uub k1; have [f2 hk2] := measure_uub k2.
+exists (f1 + f2)%R => x; rewrite /kadd /=.
+rewrite -/(measure_add (k1 x) (k2 x)).
+by rewrite measure_addE EFinD; exact: lte_add.
+Qed.
+
+HB.instance Definition _ t :=
+  Kernel_isFinite.Build _ _ _ _ R (kadd k1 k2) kadd_finite_uub.
+End fkadd.
+
+Section mnormalize.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variables (f : X -> {measure set Y -> \bar R}) (P : probability Y R).
+
+Definition mnormalize x U :=
+  let evidence := f x [set: Y] in
+  if (evidence == 0) || (evidence == +oo) then P U
+  else f x U * (fine evidence)^-1%:E.
+
+Let mnormalize0 x : mnormalize x set0 = 0.
+Proof.
+by rewrite /mnormalize; case: ifPn => // _; rewrite measure0 mul0e.
+Qed.
+
+Let mnormalize_ge0 x U : 0 <= mnormalize x U.
+Proof. by rewrite /mnormalize; case: ifPn => //; case: ifPn. Qed.
+
+Let mnormalize_sigma_additive x : semi_sigma_additive (mnormalize x).
+Proof.
+move=> F mF tF mUF; rewrite /mnormalize/=.
+case: ifPn => [_|_]; first exact: measure_semi_sigma_additive.
+rewrite (_ : (fun _ => _) = ((fun n => \sum_(0 <= i < n) f x (F i)) \*
+                          cst ((fine (f x setT))^-1)%:E)); last first.
+  by apply/funext => n; rewrite -ge0_sume_distrl.
+by apply: cvgeMr => //; exact: measure_semi_sigma_additive.
+Qed.
+
+HB.instance Definition _ x := isMeasure.Build _ _ _ (mnormalize x)
+  (mnormalize0 x) (mnormalize_ge0 x) (@mnormalize_sigma_additive x).
+
+Let mnormalize1 x : mnormalize x setT = 1.
+Proof.
+rewrite /mnormalize; case: ifPn; first by rewrite probability_setT.
+rewrite negb_or => /andP[ft0 ftoo].
+have ? : f x setT \is a fin_num.
+  by rewrite ge0_fin_numE// lt_neqAle ftoo/= leey.
+by rewrite -{1}(@fineK _ (f x setT))// -EFinM divrr// ?unitfE fine_eq0.
+Qed.
+
+HB.instance Definition _ x :=
+  Measure_isProbability.Build _ _ _ (mnormalize x) (mnormalize1 x).
+
+End mnormalize.
+
+Section knormalize.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variable f : R.-ker X ~> Y.
+
+Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} :=
+  fun x => [the measure _ _ of mnormalize f P x].
+
+Variable P : probability Y R.
+
+Let measurable_fun_knormalize U :
+  measurable U -> measurable_fun setT (knormalize P ^~ U).
+Proof.
+move=> mU; rewrite /knormalize/= /mnormalize /=.
+rewrite (_ : (fun _ => _) = (fun x =>
+     if f x setT == 0 then P U else if f x setT == +oo then P U
+     else f x U * (fine (f x setT))^-1%:E)); last first.
+  apply/funext => x; case: ifPn => [/orP[->//|->]|]; first by case: ifPn.
+  by rewrite negb_or=> /andP[/negbTE -> /negbTE ->].
+apply: measurable_fun_if => //;
+  [exact: kernel_measurable_fun_eq_cst|exact: measurable_fun_cst|].
+apply: measurable_fun_if => //.
+- rewrite setTI [X in measurable X](_ : _ = [set t | f t setT != 0]).
+    exact: kernel_measurable_neq_cst.
+  by apply/seteqP; split => [x /negbT//|x /negbTE].
+- apply: (@measurable_funS _ _ _ _ setT) => //.
+  exact: kernel_measurable_fun_eq_cst.
+- exact: measurable_fun_cst.
+- apply: emeasurable_funM.
+    by have := measurable_kernel f U mU; exact: measurable_funS.
+  apply/EFin_measurable_fun.
+  apply: (@measurable_fun_comp _ _ _ _ _ _ [set r : R | r != 0%R]) => //.
+  + exact: open_measurable.
+  + move=> /= r [t] [] [_ ft0] ftoo ftr; apply/eqP => r0.
+    move: (ftr); rewrite r0 => /eqP; rewrite fine_eq0 ?ft0//.
+    by rewrite ge0_fin_numE// lt_neqAle leey ftoo.
+  + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0.
+    exact: inv_continuous.
+  + apply: measurable_funT_comp => /=; first exact: measurable_fun_fine.
+    by have := measurable_kernel f _ measurableT; exact: measurable_funS.
+Qed.
+
+HB.instance Definition _ := isKernel.Build _ _ _ _ R (knormalize P)
+  measurable_fun_knormalize.
+
+Let knormalize1 x : knormalize P x setT = 1.
+Proof.
+rewrite /knormalize/= /mnormalize.
+case: ifPn => [_|]; first by rewrite probability_setT.
+rewrite negb_or => /andP[fx0 fxoo].
+have ? : f x setT \is a fin_num by rewrite ge0_fin_numE// lt_neqAle fxoo/= leey.
+rewrite -{1}(@fineK _ (f x setT))//=.
+by rewrite -EFinM divrr// ?lte_fin ?ltr1n// ?unitfE fine_eq0.
+Qed.
+
+HB.instance Definition _ :=
+  @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) knormalize1.
+
+End knormalize.
+
+Section kcomp_def.
+Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
+  (Z : measurableType d3) (R : realType).
+Variable l : X -> {measure set Y -> \bar R}.
+Variable k : (X * Y)%type -> {measure set Z -> \bar R}.
+
+Definition kcomp x U := \int[l x]_y k (x, y) U.
+
+End kcomp_def.
+
+Section kcomp_is_measure.
+Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
+ (Z : measurableType d3) (R : realType).
+Variable l : R.-ker X ~> Y.
+Variable k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z.
+
+Local Notation "l \; k" := (kcomp l k).
+
+Let kcomp0 x : (l \; k) x set0 = 0.
+Proof.
+by rewrite /kcomp (eq_integral (cst 0)) ?integral0// => y _; rewrite measure0.
+Qed.
+
+Let kcomp_ge0 x U : 0 <= (l \; k) x U. Proof. exact: integral_ge0. Qed.
+
+Let kcomp_sigma_additive x : semi_sigma_additive ((l \; k) x).
+Proof.
+move=> U mU tU mUU; rewrite [X in _ --> X](_ : _ =
+  \int[l x]_y (\sum_(n <oo) k (x, y) (U n))); last first.
+  apply: eq_integral => V _.
+  by apply/esym/cvg_lim => //; exact/measure_semi_sigma_additive.
+apply/cvg_closeP; split.
+  by apply: is_cvg_nneseries => n _; exact: integral_ge0.
+rewrite closeE// integral_nneseries// => n.
+by have /measurable_fun_prod1 := measurable_kernel k _ (mU n).
+Qed.
+
+HB.instance Definition _ x := isMeasure.Build _ R _
+  ((l \; k) x) (kcomp0 x) (kcomp_ge0 x) (@kcomp_sigma_additive x).
+
+Definition mkcomp : X -> {measure set Z -> \bar R} := fun x =>
+  [the measure _ _ of (l \; k) x].
+
+End kcomp_is_measure.
+
+Notation "l \; k" := (mkcomp l k) : ereal_scope.
+
+Module KCOMP_FINITE_KERNEL.
+
+Section kcomp_finite_kernel_kernel.
+Context d d' d3 (X : measurableType d) (Y : measurableType d')
+  (Z : measurableType d3) (R : realType) (l : R.-fker X ~> Y)
+  (k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z).
+
+Lemma measurable_fun_kcomp_finite U :
+  measurable U -> measurable_fun setT ((l \; k) ^~ U).
+Proof.
+move=> mU; apply: (measurable_fun_integral_finite_kernel (k ^~ U)) => //=.
+exact/measurable_kernel.
+Qed.
+
+HB.instance Definition _ :=
+  isKernel.Build _ _ X Z R (l \; k) measurable_fun_kcomp_finite.
+
+End kcomp_finite_kernel_kernel.
+
+Section kcomp_finite_kernel_finite.
+Context d d' d3 (X : measurableType d) (Y : measurableType d')
+  (Z : measurableType d3) (R : realType).
+Variable l : R.-fker X ~> Y.
+Variable k : R.-fker [the measurableType _ of (X * Y)%type] ~> Z.
+
+Let mkcomp_finite : measure_fam_uub (l \; k).
+Proof.
+have /measure_fam_uubP[r hr] := measure_uub k.
+have /measure_fam_uubP[s hs] := measure_uub l.
+apply/measure_fam_uubP; exists (PosNum [gt0 of (r%:num * s%:num)%R]) => x /=.
+apply: (@le_lt_trans _ _ (\int[l x]__ r%:num%:E)).
+  apply: ge0_le_integral => //.
+  - have /measurable_fun_prod1 := measurable_kernel k _ measurableT.
+    exact.
+  - exact/measurable_fun_cst.
+  - by move=> y _; exact/ltW/hr.
+by rewrite integral_cst//= EFinM lte_pmul2l.
+Qed.
+
+HB.instance Definition _ :=
+  Kernel_isFinite.Build _ _ X Z R (l \; k) mkcomp_finite.
+
+End kcomp_finite_kernel_finite.
+End KCOMP_FINITE_KERNEL.
+
+Section kcomp_sfinite_kernel.
+Context d d' d3 (X : measurableType d) (Y : measurableType d')
+  (Z : measurableType d3) (R : realType).
+Variable l : R.-sfker X ~> Y.
+Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z.
+
+Import KCOMP_FINITE_KERNEL.
+
+Lemma mkcomp_sfinite : exists k_ : (R.-fker X ~> Z)^nat,
+  forall x U, measurable U -> (l \; k) x U = kseries k_ x U.
+Proof.
+have [k_ hk_] := sfinite k; have [l_ hl_] := sfinite l.
+have [kl hkl] : exists kl : (R.-fker X ~> Z) ^nat, forall x U,
+    \esum_(i in setT) (l_ i.2 \; k_ i.1) x U = \sum_(i <oo) kl i x U.
+  have /ppcard_eqP[f] : ([set: nat] #= [set: nat * nat])%card.
+    by rewrite card_eq_sym; exact: card_nat2.
+  exists (fun i => [the _.-fker _ ~> _ of l_ (f i).2 \; k_ (f i).1]) => x U.
+  by rewrite (reindex_esum [set: nat] _ f)// nneseries_esum// fun_true.
+exists kl => x U mU.
+transitivity (([the _.-ker _ ~> _ of kseries l_] \;
+               [the _.-ker _ ~> _ of kseries k_]) x U).
+  rewrite /= /kcomp [in RHS](eq_measure_integral (l x)); last first.
+    by move=> *; rewrite hl_.
+  by apply: eq_integral => y _; rewrite hk_.
+rewrite /= /kcomp/= integral_nneseries//=; last first.
+  move=> n; have /measurable_fun_prod1 := measurable_kernel (k_ n) _ mU.
+   exact.
+transitivity (\sum_(i <oo) \sum_(j <oo) (l_ j \; k_ i) x U).
+  apply: eq_eseriesr => i _; rewrite integral_kseries//.
+  by have /measurable_fun_prod1 := measurable_kernel (k_ i) _ mU; exact.
+rewrite /mseries -hkl/=.
+rewrite (_ : setT = setT `*`` (fun=> setT)); last by apply/seteqP; split.
+rewrite -(@esum_esum _ _ _ _ _ (fun i j => (l_ j \; k_ i) x U))//.
+rewrite nneseries_esum; last by move=> n _; exact: nneseries_ge0.
+by rewrite fun_true; apply: eq_esum => /= i _; rewrite nneseries_esum// fun_true.
+Qed.
+
+Lemma measurable_fun_mkcomp_sfinite U : measurable U ->
+  measurable_fun setT ((l \; k) ^~ U).
+Proof.
+move=> mU; apply: (measurable_fun_integral_sfinite_kernel (k ^~ U)) => //.
+exact/measurable_kernel.
+Qed.
+
+End kcomp_sfinite_kernel.
+
+Module KCOMP_SFINITE_KERNEL.
+Section kcomp_sfinite_kernel.
+Context d d' d3 (X : measurableType d) (Y : measurableType d')
+  (Z : measurableType d3) (R : realType).
+Variable l : R.-sfker X ~> Y.
+Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z.
+
+HB.instance Definition _ :=
+  isKernel.Build _ _ X Z R (l \; k) (measurable_fun_mkcomp_sfinite l k).
+
+#[export]
+HB.instance Definition _ :=
+  Kernel_isSFinite.Build _ _ X Z R (l \; k) (mkcomp_sfinite l k).
+
+End kcomp_sfinite_kernel.
+End KCOMP_SFINITE_KERNEL.
+HB.export KCOMP_SFINITE_KERNEL.
+
+Section measurable_fun_preimage_integral.
+Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
+Variables (k : Y -> \bar R)
+  (k_ : ({nnsfun Y >-> R}) ^nat)
+  (ndk_ : nondecreasing_seq (k_ : (Y -> R)^nat))
+  (k_k : forall z, setT z -> EFin \o (k_ ^~ z) --> k z).
+
+Let k_2 : (X * Y -> R)^nat := fun n => k_ n \o snd.
+
+Let k_2_ge0 n x : (0 <= k_2 n x)%R. Proof. by []. Qed.
+
+HB.instance Definition _ n := @isNonNegFun.Build _ _ _ (k_2_ge0 n).
+
+Let mk_2 n : measurable_fun setT (k_2 n).
+Proof. by apply: measurable_funT_comp => //; exact: measurable_fun_snd. Qed.
+
+HB.instance Definition _ n := @isMeasurableFun.Build _ _ _ _ (mk_2 n).
+
+Let fk_2 n : finite_set (range (k_2 n)).
+Proof.
+have := @fimfunP _ _ (k_ n).
+suff : range (k_ n) = range (k_2 n) by move=> <-.
+by apply/seteqP; split => r [y ?] <-; [exists (point, y)|exists y.2].
+Qed.
+
+HB.instance Definition _ n := @FiniteImage.Build _ _ _ (fk_2 n).
+
+Lemma measurable_fun_preimage_integral (l : X -> {measure set Y -> \bar R}) :
+  (forall n r, measurable_fun setT (l ^~ (k_ n @^-1` [set r]))) ->
+  measurable_fun setT (fun x => \int[l x]_z k z).
+Proof.
+move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l
+  (fun n => [the {nnsfun _ >-> _} of k_2 n])) => /=.
+- by rewrite /k_2 => m n mn; apply/lefP => -[x y] /=; exact/lefP/ndk_.
+- by move=> [x y]; exact: k_k.
+- move=> n r _ /= B mB.
+  have := h n r measurableT B mB; rewrite !setTI.
+  suff : (l ^~ (k_ n @^-1` [set r])) @^-1` B =
+         (fun x => l x (xsection (k_2 n @^-1` [set r]) x)) @^-1` B by move=> ->.
+  by apply/seteqP; split => x/=;
+    rewrite (comp_preimage _ snd (k_ n)) xsection_preimage_snd.
+Qed.
+
+End measurable_fun_preimage_integral.
+
+Lemma measurable_fun_integral_kernel
+    d d' (X : measurableType d) (Y : measurableType d') (R : realType)
+    (l : X -> {measure set Y -> \bar R})
+    (ml : forall U, measurable U -> measurable_fun setT (l ^~ U))
+    (* NB: l is really just a kernel *)
+    (k : Y -> \bar R) (k0 : forall z, 0 <= k z) (mk : measurable_fun setT k) :
+  measurable_fun setT (fun x => \int[l x]_y k y).
+Proof.
+have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x).
+by apply: (measurable_fun_preimage_integral ndk_ k_k) => n r; exact/ml.
+Qed.
+
+Section integral_kcomp.
+Context d d2 d3 (X : measurableType d) (Y : measurableType d2)
+  (Z : measurableType d3) (R : realType).
+Variables (l : R.-sfker X ~> Y)
+          (k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z).
+
+Let integral_kcomp_indic x E (mE : measurable E) :
+  \int[(l \; k) x]_z (\1_E z)%:E = \int[l x]_y (\int[k (x, y)]_z (\1_E z)%:E).
+Proof.
+rewrite integral_indic//= /kcomp.
+by apply: eq_integral => y _; rewrite integral_indic.
+Qed.
+
+Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) :
+  \int[(l \; k) x]_z (f z)%:E = \int[l x]_y (\int[k (x, y)]_z (f z)%:E).
+Proof.
+under [in LHS]eq_integral do rewrite fimfunE -fsumEFin//.
+rewrite ge0_integral_fsum//; last 2 first.
+  - move=> r; apply/EFin_measurable_fun/measurable_funrM.
+    have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP.
+    by rewrite (_ : \1__ = mindic R fr).
+  - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0.
+under [in RHS]eq_integral.
+  move=> y _.
+  under eq_integral.
+    by move=> z _; rewrite fimfunE -fsumEFin//; over.
+  rewrite /= ge0_integral_fsum//; last 2 first.
+    - move=> r; apply/EFin_measurable_fun/measurable_funrM.
+      have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP.
+      by rewrite (_ : \1__ = mindic R fr).
+    - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0.
+  under eq_fsbigr.
+    move=> r _.
+    rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first.
+      by move=> r0; rewrite preimage_nnfun0.
+    rewrite integral_indic// setIT.
+    over.
+  over.
+rewrite /= ge0_integral_fsum//; last 2 first.
+  - move=> r; apply: measurable_funeM.
+    have := measurable_kernel k (f @^-1` [set r])
+            (measurable_sfunP f (measurable_set1 r)).
+    by move=> /measurable_fun_prod1; exact.
+  - move=> n y _.
+    have := mulemu_ge0 (fun n => f @^-1` [set n]).
+    by apply; exact: preimage_nnfun0.
+apply: eq_fsbigr => r _.
+rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first.
+  exact: preimage_nnfun0.
+rewrite /= integral_kcomp_indic; last exact/measurable_sfunP.
+have [r0|r0] := leP 0%R r.
+  rewrite ge0_integralM//; last first.
+    have := measurable_kernel k (f @^-1` [set r])
+            (measurable_sfunP f (measurable_set1 r)).
+    by move/measurable_fun_prod1; exact.
+  by congr (_ * _); apply: eq_integral => y _; rewrite integral_indic// setIT.
+rewrite integral0_eq ?mule0; last first.
+   move=> y _; rewrite integral0_eq// => z _.
+   by rewrite preimage_nnfun0// indic0.
+by rewrite integral0_eq// => y _; rewrite preimage_nnfun0// measure0 mule0.
+Qed.
+
+Lemma integral_kcomp x f : (forall z, 0 <= f z) -> measurable_fun setT f ->
+  \int[(l \; k) x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z).
+Proof.
+move=> f0 mf.
+have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z).
+transitivity (\int[(l \; k) x]_z (lim (EFin \o f_^~ z))).
+  by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f.
+rewrite monotone_convergence//; last 3 first.
+  by move=> n; exact/EFin_measurable_fun.
+  by move=> n z _; rewrite lee_fin.
+  by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin.
+rewrite (_ : (fun _ => _) =
+    (fun n => \int[l x]_y (\int[k (x, y)]_z (f_ n z)%:E)))//; last first.
+  by apply/funext => n; rewrite integral_kcomp_nnsfun.
+transitivity (\int[l x]_y lim (fun n => \int[k (x, y)]_z (f_ n z)%:E)).
+  rewrite -monotone_convergence//; last 3 first.
+  - move=> n; apply: measurable_fun_integral_kernel => //.
+    + move=> U mU; have := measurable_kernel k _ mU.
+      by move=> /measurable_fun_prod1; exact.
+    + by move=> z; rewrite lee_fin.
+    + exact/EFin_measurable_fun.
+  - by move=> n y _; apply: integral_ge0 => // z _; rewrite lee_fin.
+  - move=> y _ a b ab; apply: ge0_le_integral => //.
+    + by move=> z _; rewrite lee_fin.
+    + exact/EFin_measurable_fun.
+    + by move=> z _; rewrite lee_fin.
+    + exact/EFin_measurable_fun.
+    + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin.
+apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first.
+  - by move=> n; exact/EFin_measurable_fun.
+  - by move=> n z _; rewrite lee_fin.
+  - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin.
+by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f.
+Qed.
+
+End integral_kcomp.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 2fb442d89e..0d1aa2cd02 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -4029,8 +4029,12 @@ Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
 Implicit Types A : set (T1 * T2).
 
 Section xsection.
-Variables (pt2 : T2) (m2 : {measure set T2 -> \bar R}).
-Let phi A := m2 \o xsection A.
+Variables (pt2 : T2) (m2 : T1 -> {measure set T2 -> \bar R}).
+(* the generalization from m2 : {measure set T2 -> \bar R}t to
+   T1 -> {measure set T2 -> \bar R} is needed to develop the theory
+   of kernels; the original type was sufficient for the development
+   of the theory of integration  *)
+Let phi A x := m2 x (xsection A x).
 Let B := [set A | measurable A /\ measurable_fun setT (phi A)].
 
 Lemma xsection_ndseq_closed : ndseq_closed B.