theorem Th31: :: GROUP_23:34

for I being non empty set
for i being Element of I
for F being Group-Family of I holds proj ((Carrier F),i) is Function of (product (Carrier F)), the carrier of (F . i)