theorem Th39: :: GROUP_23:42

for I being non empty set
for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F ex phi being Homomorphism of G,(product F) st
for g being Element of G
for j being Element of I holds (f . j) . g = (proj (F,j)) . (phi . g)