theorem Th9: :: GROUP_23:14

for I being non empty set
for i being Element of I
for F being Group-Family of I holds (Carrier F) . i = the carrier of (F . i)