theorem Th38: :: GROUP_23:41

for I being non empty set
for i being Element of I
for F being Group-Family of I holds (proj (F,i)) * (1ProdHom (F,i)) = id the carrier of (F . i)