diff --git a/set.mm b/set.mm
index 7f934d8de5..99acff5296 100644
--- a/set.mm
+++ b/set.mm
@@ -214990,7 +214990,7 @@ is an important property of monoids (see ~ mndid ), and therefore also for
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-  Group sum operation for magmas
+  Group sum operation in magmas
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
 
   The symbol ` gsum ` is mostly used in the context of abelian groups.
@@ -216933,7 +216933,7 @@ proposition to be be proved (the first four hypotheses tell its values
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-  Group sum operation for monoids
+  Group sum operation in monoids
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
 
   One important use of words is as formal composites in cases where order is
@@ -735203,29 +735203,37 @@ their group (addition) operations are equal for all pairs of elements of
   $}
 
   ${
-    $d B x y $.  $d L x y $.  $d R x y $.  $d G y $.  $d .+ x y $.  $d .0. y $.
-    lidridid.b $e |- B = ( Base ` G ) $.
-    lidridid.p $e |- .+ = ( +g ` G ) $.
-    lidridid.o $e |- .0. = ( 0g ` G ) $.
-    $( If a magma has a left and right identity element, both identity elements
-       are equal and are equal to "the" identity element.  Generalization of
-       statement in [Lang] p. 3: it is sufficient that "e" is a left identity
-       element and "e``" is a right identity element instead of both being
-       (two-sided) identity elements.  (Contributed by AV, 26-Dec-2023.) $)
-    lidridid $p |- ( ( L e. B /\ R e. B )
-                     -> ( A. x e. B ( ( L .+ x ) = x /\ ( x .+ R ) = x )
-                          -> ( L = R /\ L = .0. ) ) ) $=
-      ( vy co wceq wa wral wcel wi oveq2 eqeq12d rspcv cv r19.26 id oveq1 eqtr2
-      w3a adantl ex syl6 adantr com23 syld simpr simpl1l weq com12 3ad2ant2 imp
-      3imp eqcoms eqeq1d biimpcd com3l 3ad2ant3 imp31 ismgmid2 jca mpdan 3expib
-      syl5bi ) FAUAZCLZVKMZVKDCLZVKMZNABOVMABOZVOABOZNFBPZDBPZNZFDMZFGMZNZVMVOA
-      BUBVTVPVQWCVTVPVQUFZWAWCVTVPVQWAVTVPFDCLZDMZVQWAQVSVPWFQVRVMWFADBVKDMZVLW
-      EVKDVKDFCRWGUCSTUGVTVQWFWAVRVQWFWAQZQVSVRVQWEFMZWHVOWIAFBVKFMZVNWEVKFVKFD
-      CUDWJUCSTWIWFWAWEFDUEUHUIUJUKULUSWDWANZWAWBWDWAUMWKKBCFEGHJIVRVSVPVQWAUNW
-      KKUAZBPZFWLCLZWLMZWDWMWOQZWAVPVTWPVQWMVPWOVMWOAWLBAKUOZVLWNVKWLVKWLFCRWQU
-      CZSTUPUQUJURWDWAWMWLFCLZWLMZVQVTWAWMWTQQVPWMVQWAWTWMVQWLDCLZWLMZWAWTQVOXB
-      AWLBWQVNXAVKWLVKWLDCUDWRSTWAXBWTWAXAWSWLXAWSMDFDFWLCRUTVAVBUIVCVDVEVFVGVH
-      VIVJ $.
+    $d B x $.  $d L x $.  $d R x $.  $d .+ x $.
+    lidrideqd.l $e |- ( ph -> L e. B ) $.
+    lidrideqd.r $e |- ( ph -> R e. B ) $.
+    lidrideqd.li $e |- ( ph -> A. x e. B ( L .+ x ) = x ) $.
+    lidrideqd.ri $e |- ( ph -> A. x e. B ( x .+ R ) = x ) $.
+    $( If there is a left and right identity element for any binary operation
+       (group operation) ` .+ ` , both identity elements are equal.
+       Generalization of statement in [Lang] p. 3: it is sufficient that "e" is
+       a left identity element and "e``" is a right identity element instead of
+       both being (two-sided) identity elements.  (Contributed by AV,
+       26-Dec-2023.) $)
+    lidrideqd $p |- ( ph -> L = R ) $=
+      ( co cv wceq oveq1 id eqeq12d rspcdva oveq2 eqtr3d ) AFEDKZFEABLZEDKZUAMT
+      FMBCFUAFMZUBTUAFUAFEDNUCOPJGQAFUADKZUAMTEMBCEUAEMZUDTUAEUAEFDRUEOPIHQS $.
+
+    $d B x y $.  $d L y $.  $d R y $.  $d G y $.  $d .+ y $.  $d .0. y $.
+    $d ph y $.
+    lidrideqd.b $e |- B = ( Base ` G ) $.
+    lidrideqd.p $e |- .+ = ( +g ` G ) $.
+    lidrididd.o $e |- .0. = ( 0g ` G ) $.
+    $( If there is a left and right identity element for any binary operation
+       (group operation) ` .+ ` , the left identity element (and therefore also
+       the right identity element according to ~ lidrideqd ) is equal to the
+       two-sided identity element.  (Contributed by AV, 26-Dec-2023.) $)
+    lidrididd $p |- ( ph -> L = .0. ) $=
+      ( vy cv co wceq wral wcel oveq2 id eqeq12d rspcv mpan9 wi lidrideqd oveq1
+      weq wa adantl simpl eqtrd ex syl6com com23 sylc imp ismgmid2 ) APCDGFHMON
+      IAGBQZDRZVASZBCTPQZCUAZGVDDRZVDSZKVCVGBVDCBPUJZVBVFVAVDVAVDGDUBVHUCZUDUEU
+      FAVEVDGDRZVDSZAVAEDRZVASZBCTZGESZVEVKUGLABCDEGIJKLUHVNVEVOVKVEVNVDEDRZVDS
+      ZVOVKUGVMVQBVDCVHVLVPVAVDVAVDEDUIVIUDUEVQVOVKVQVOUKVJVPVDVOVJVPSVQGEVDDUB
+      ULVQVOUMUNUOUPUQURUSUT $.
   $}
 
   ${
@@ -736040,10 +736048,10 @@ Group sum operation (extension 1)
     gsumfsupp.a $e |- ( ph -> A e. V ) $.
     gsumfsupp.f $e |- ( ph -> F : A --> B ) $.
     gsumfsupp.w $e |- ( ph -> F finSupp .0. ) $.
-    $( A group sum is identical with the group sum restricted to the finite
-       support of its index set.  This corresponds to the definition of an
-       (infinite) product in [Lang] p. 5, two last formulas.  (Contributed by
-       AV, 27-Dec-2023.) $)
+    $( A group sum of a family can be restricted to the support of that family
+       without changing its value, provided that that support is finite.  This
+       corresponds to the definition of an (infinite) product in [Lang] p. 5,
+       last two formulas.  (Contributed by AV, 27-Dec-2023.) $)
     gsumfsupp $p |- ( ph -> ( G gsum ( F |` I ) ) = ( G gsum F ) ) $=
       ( csupp co wss eqimss2i a1i gsumres ) ABCDEGFHIJLMNDHPQZFRAFUBKSTOUA $.
   $}
@@ -736118,7 +736126,7 @@ Group multiple operation (extension) and cyclic monoids
     cycsubm.f $e |- F = ( x e. NN0 |-> ( x .x. A ) ) $.
     cycsubm.c $e |- C = ran F $.
     $( Characterization of an element of the set of nonnegative integer powers
-       of an element ` A ` of a monoid.  (Contributed by AV, 28-Dec-2023.) $)
+       of an element ` A ` of a magma.  (Contributed by AV, 28-Dec-2023.) $)
     cycsubmel $p |- ( X e. C <-> E. i e. NN0 X = ( i .x. A ) ) $=
       ( wcel cv wceq cn0 wrex co ovex crn cfv eleq2i wfn wb fvelrnb ax-mp oveq1
       fnmpti fvmpt eqeq1d eqcom syl6bb rexbiia 3bitri ) IDNIGUAZNZFOZGUBZIPZFQR
@@ -736126,7 +736134,7 @@ Group multiple operation (extension) and cyclic monoids
       VCVFUSVBIAURVEVBQGVDURBEUHLURBETUJUKVBIULUMUNUO $.
 
     $d A i $.  $d B i $.  $d .x. i $.
-    $( The set of nonnegative integer powers of an element ` A ` of a monoid
+    $( The set of nonnegative integer powers of an element ` A ` of a magma
        contains ` A ` .  (Contributed by AV, 28-Dec-2023.) $)
     cycsubmcl $p |- ( A e. B -> A e. C ) $=
       ( vi wcel cv co wceq cn0 wrex c1 1nn0 wb oveq1 eqeq2d adantl mulg1 eqcomd