theorem :: GROUP_23:11

for I being set
for F being ManySortedSet of I holds
( F is Group-yielding iff for i being object st i in I holds
F . i is Group )