theorem Th42: :: GROUP_23:45

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
for g being Element of G holds
( ( for i being Element of I holds ((product f) . g) . i = 1_ (F . i) ) iff (product f) . g = 1_ (product F) )