Definition 2.6.16.  Let G be an abeliangroup. We define
G
by:
Example.

$../../Essentials/Operations/"Iterated operations"/"indexed by natural number"(X = $Carrier(𝐆 = 𝐆), ⨂ = $"iterated operation"(𝐆 = 𝐆), n = n, _1 = {#(i: %Element($../../Essentials/Numbers/Natural/Subsets/"Segment (less)"(n = n))), {a = {a[i = i]}}})

References.