Add compose3.

Lebesgue/Set_theory/Set_def_fun_base.v

@@ -37,7 +37,7 @@ Definition bijective_alt : Prop := forall x2, exists! x1, f x1 = x2.
 End Fun_Base_Def1.
 
 
-Section Fun_Base_Def2.
+Section Fun_Base_Def2a.
 
 Context {U1 U2 U3 : Type}. (* Universes. *)
 Variable f23 : U2 -> U3.
@@ -45,7 +45,19 @@ Variable f12 : U1 -> U2.
 
 Definition compose : U1 -> U3 := fun x1 => f23 (f12 x1).
 
-End Fun_Base_Def2.
+End Fun_Base_Def2a.
+
+
+Section Fun_Base_Def2b.
+
+Context {U1 U2 U3 U4 : Type}. (* Universes. *)
+Variable f34 : U3 -> U4.
+Variable f23 : U2 -> U3.
+Variable f12 : U1 -> U2.
+
+Definition compose3 : U1 -> U4 := compose f34 (compose f23 f12).
+
+End Fun_Base_Def2b.
 
 
 Section Fun_Base_Def3.
@@ -157,7 +169,7 @@ End Fun_Base_Facts2.
 Ltac fun_unfold :=
   repeat unfold
     bijective, surjective, injective_alt, injective, same_fun, (* Predicate. *)
-      compose, preimage, image_ex. (* Operators. *)
+      compose3, compose, preimage, image_ex. (* Operators. *)
 
 Ltac fun_auto :=
   fun_unfold; set_auto.