for I being non empty set
for G being Group
for i being object st i in I holds
ex F being Group-Family of I ex h being Homomorphism of (sum F),G st
( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ (product F)) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) )