diff --git a/Lebesgue/Function.v b/Lebesgue/Function.v
index 3084cf53cf3725864c7907acbf04fc7960238916..d2f53cff95f06dad8c5dc7163970607e02f19cb5 100644
--- a/Lebesgue/Function.v
+++ b/Lebesgue/Function.v
@@ -47,8 +47,8 @@ Definition preimage : U1 -> Prop := fun x1 => A2 (f x1).
 
 Context {U3 : Type}. (* Universe. *)
 
-Variable f12 : U1 -> U2. (* Function. *)
 Variable f23 : U2 -> U3. (* Function. *)
+Variable f12 : U1 -> U2. (* Function. *)
 
 Definition compose : U1 -> U3 := fun x1 => f23 (f12 x1).