:: deftheorem Def9 defines sum GROUP_7:def 9 :
for I being set
for F being Group-like associative multMagma-Family of I
for b₃ being strict Subgroup of product F holds
( b₃ = sum F iff for x being object holds
( x in the carrier of b₃ iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) );