theorem Th7: :: GROUP_19:7

for I being set
for F being Group-Family of I
for a being Element of (sum F) ex J being finite Subset of I ex b being ManySortedSet of J st
( J = support (a,F) & a = (1_ (product F)) +* b & ( for j being object
for G being Group st j in I \ J & G = F . j holds
a . j = 1_ G ) & ( for j being object st j in J holds
a . j = b . j ) )