theorem :: GROUP_23:44

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 phi1, phi2 being Homomorphism of G,(product F) st ( for i being Element of I holds f . i = (proj (F,i)) * phi1 ) & ( for i being Element of I holds f . i = (proj (F,i)) * phi2 ) holds
phi1 = phi2