for I being non empty set
for J being disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for j being Element of I
for i being object st i in J . j holds
(Union F) . i = (F . j) . i