theorem Th2: :: GROUP_20:2

for I being non empty set
for G being Group
for F being Group-Family of I
for x being Function of I,G st x in product F holds
x is Function of I,(Union (Carrier F))