:: deftheorem Def14 defines product GROUP_23:def 14 :
for G being Group
for I being non empty set
for F being Group-Family of I
for f being Homomorphism-Family of G,F
for b₅ being Homomorphism of G,(product F) holds
( b₅ = product f iff for g being Element of G
for i being Element of I holds (f . i) . g = (b₅ . g) . i );