Appropriate names for +g and gsum

Currently, +g is called "group operation" (see ~df-plusg), and gsum is called "group sum" (see ~df-gsum), or "finitely supported group sum" (see constant definition ~cgsu).

Since these symbols are (or at least can be) meaningful not only for groups, but also for magmas, monoids, etc., their names should be more general (see also discussion in #3724).

For gsum, there was already a discussion in #1457, where "ordered sum" was proposed. The term "ordered", however, seems to be too restrictive, because gsum is also defined for arbitrary (unordered) finite sets, see ~gsumval3 (this may make sense only if all involved elements commute). In Bourbaki (Algebra I, definition 4 on page 3), the term "composition ... of the ordered sequence ..." is used. Unlike gsum, however, this definition cannot be used for arbitrary finite sets.

According to Wikipedia, "Iterated binary operation" would be an appropriate name (see https://en.wikipedia.org/wiki/Iterated_binary_operation), this would be consistent if +g would be called "binary operation" (see also https://en.wikipedia.org/wiki/Binary_operation) instead of "group operation" (however, the term "binary operation" is already used in set.mm for arbitrary functions ( S X S ) -> M, not only for functions ( S X S ) -> S). In https://planetmath.org/binaryoperation, the term "internal composition" is used for +g, whereas in https://www.mathyma.com/mathsNotes/index.php?lng=en&trg=S1C2_Struct_IntBinOp it is called "internal binary operation".

To summarize, here are some proposals for new names (first for +g, second for gsum):

binary operation - iterated binary operation (according to Wikipedia)
internal binary operation - iterated binary operation (combination of Wikipedia and Mathyma)
internal composition - iterated composition (combination of Wikipedia and Planetmath)
law of composition - iterated composition (combination of Wikipedia and Bourbaki, name for gsum also proposed by @benjub in #3724)
magma operation - magma sum (current names generalized)

I propose the following, which refers to the two definitions I gave in https://github.com/metamath/set.mm/issues/3727#issuecomment-1872602828:

  $( Definition of the iterated composition of a finite sequence of elements in
     an extensible structure (see ~ df-struct ).  It iterates the group-like
     operation of the extensible structure (see ~ df-plusg ), so it could also
     be called the "iterated group-like operation".  These terms are not
     standard because they should apply to various cases: for instance, when
     the structure is an additive (resp. multiplicative) group, this is simply
     the sum (resp. product) of a (finite) sequence of elements of the group.

     Since the group-like operation need not be associative nor commutative,
     the order and grouping of elements of the family matter.  We choose
     leftmost grouping, that is, the sequence of elements ` a , b , c , d ` is
     composed as ` ( ( ( a + b ) + c ) + d ) ` ......

  df-gsum $a |- gsum = ( w e. _V , f e. _V |-> [_ { x e. ( Base ` w ) |

metamath / set.mm

Appropriate names for +g and gsum #3726