From 795b6b70d4975fbd871ab118fb754e15e7c6a01d Mon Sep 17 00:00:00 2001
From: Jim Kingdon <kingdon@panix.com>
Date: Mon, 23 Dec 2024 23:01:31 -0700
Subject: [PATCH] copy submmulgcl from set.mm to iset.mm

---
 iset.mm | 12 ++++++++++++
 1 file changed, 12 insertions(+)

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 $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#