:: deftheorem Def15 defines product GROUP_23:def 16 :
for I being non empty set
for F1, F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2
for b₅ being Homomorphism of (product F1),(product F2) holds
( b₅ = product f iff for i being Element of I holds (proj (F2,i)) * b₅ = (f . i) * (proj (F1,i)) );