diff --git a/Lebesgue/Set_theory/Sets.v b/Lebesgue/Set_theory/Sets.v
index 673aaabaa2096fe7a6f3cbb0f0dc5d13f885b95f..85094e70fefb393efcf6d3e0f6b294d0222dd2a0 100644
--- a/Lebesgue/Set_theory/Sets.v
+++ b/Lebesgue/Set_theory/Sets.v
@@ -41,5 +41,5 @@ From Coq Require Import Classical.
 
 Require Export FinBij.
 Require Export Set_def.
-Require Export Set_base Set_any Set_finite Set_seq.
+Require Export Set_fun Set_base Set_any Set_finite Set_seq.
 Require Export Set_dec Set_charac.