diff --git a/modules/Functions.tla b/modules/Functions.tla
index 29a30f8..4ea2c78 100644
--- a/modules/Functions.tla
+++ b/modules/Functions.tla
@@ -45,6 +45,23 @@ RestrictValues(f, Test(_)) ==
   LET S == {x \in DOMAIN f : Test(f[x])}
   IN  Restrict(f, S)
 
+(***************************************************************************)
+(* Check if a function narrow is a restriction of a function wide, i.e.    *)
+(* Is the domain of narrow a subset of that of wide, and does the          *)
+(* projection of wide on the domain of narrow have the same image as       *)
+(* narrow does.                                                            *)
+(*                                                                         *)
+(* Examples:                                                               *)
+(*   IsRestriction([one |-> 1], [one |-> 1, two |-> 2])                    *)
+(*   IsRestriction([one |-> 1], [one |-> 1])                               *)
+(*  ~IsRestriction([one |-> 1, two |-> 2], [one |-> 1, two |-> 3])         *)
+(*  ~IsRestriction([one |-> 1], [2 |-> two])                               *)
+(*  ~IsRestriction([one |-> 1, two |-> 2], [two |-> 2])                    *)
+(***************************************************************************)
+IsRestriction(narrow, wide) ==
+    /\ DOMAIN narrow \subseteq DOMAIN wide 
+    /\ \A x \in DOMAIN narrow \intersect DOMAIN wide: narrow[x] = wide[x]
+
 (***************************************************************************)
 (* Range of a function.                                                    *)
 (* Note: The image of a set under function f can be defined as             *)
@@ -150,23 +167,6 @@ FoldFunctionOnSet(op(_,_), base, fun, indices) ==
   (***************************************************************************)
   MapThenFoldSet(op, base, LAMBDA i : fun[i], LAMBDA s: CHOOSE x \in s : TRUE, indices)
 
-  (***************************************************************************)
-  (* Check if a function narrow is a restriction of a function wide, i.e.    *)
-  (* Is the domain of narrow a subset of that of wide, and does the          *)
-  (* projection of wide on the domain of narrow have the same image as       *)
-  (* narrow does.                                                            *)
-  (*                                                                         *)
-  (* Examples:                                                               *)
-  (*   IsRestriction([one |-> 1], [one |-> 1, two |-> 2])                    *)
-  (*   IsRestriction([one |-> 1], [one |-> 1])                               *)
-  (*  ~IsRestriction([one |-> 1, two |-> 2], [one |-> 1, two |-> 3])         *)
-  (*  ~IsRestriction([one |-> 1], [2 |-> two])                               *)
-  (*  ~IsRestriction([one |-> 1, two |-> 2], [two |-> 2])                    *)
-  (***************************************************************************)
-IsRestriction(narrow, wide) ==
-    /\ DOMAIN narrow \subseteq DOMAIN wide
-    /\ \A x \in DOMAIN narrow: narrow[x] = wide[x]
-
 =============================================================================
 \* Modification History
 \* Last modified Tue Nov 01 08:46:11 CET 2022 by merz
diff --git a/tests/FunctionsTests.tla b/tests/FunctionsTests.tla
index 3a0dae3..a05d7b5 100644
--- a/tests/FunctionsTests.tla
+++ b/tests/FunctionsTests.tla
@@ -107,10 +107,13 @@ ASSUME
         g == ("a" :> 1 @@ "b" :> 1 @@ "c" :> 3)
     IN Pointwise(f,g,-) = ("a" :> 0 @@ "b" :> 0 @@ "c" :> (-1) )
 
+ASSUME IsRestriction(<<>>, <<>>)
+ASSUME IsRestriction(<<>>, [one |-> 1])
 ASSUME IsRestriction([one |-> 1], [one |-> 1, two |-> 2])
 ASSUME IsRestriction([one |-> 1], [one |-> 1])
-ASSUME ~IsRestriction([one |-> 1, two |-> 2], [one |-> 1, two |-> 3])
+ASSUME ~IsRestriction([one |-> 1], <<>>)
 ASSUME ~IsRestriction([one |-> 1], [two |-> 2])
 ASSUME ~IsRestriction([one |-> 1, two |-> 2], [two |-> 2])
+ASSUME ~IsRestriction([one |-> 1, two |-> 2], [one |-> 1, two |-> 3])
 
 =============================================================================