diff --git a/iset.mm b/iset.mm
index 6c56510de6..7bea1c528d 100644
--- a/iset.mm
+++ b/iset.mm
@@ -147199,6 +147199,18 @@ since the target of the homomorphism (operator ` O ` in our model) need
       VPVQVRVSVT $.
   $}
 
+  ${
+    $d x y G $.  $d x y N $.  $d x y S $.  $d x .xb $.  $d x y X $.
+    submmulgcl.t $e |- .xb = ( .g ` G ) $.
+    $( Closure of the group multiple (exponentiation) operation in a submonoid.
+       (Contributed by Mario Carneiro, 13-Jan-2015.) $)
+    submmulgcl $p |- ( ( S e. ( SubMnd ` G ) /\ N e. NN0 /\ X e. S ) ->
+      ( N .xb X ) e. S ) $=
+      ( vx vy csubmnd cfv wcel cbs cplusg cmnd c0g eqid submrcl submss submcl
+      cv subm0cl mulgnn0subcl ) ACIJKGHCLJZCMJZABCDNECOJZUCPZFUDPZACQUCACUFRUDA
+      CGTHTUGSUEPZACUEUHUAUB $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#