:: deftheorem Def2 defines product GROUP_7:def 2 :
for I being set
for F being multMagma-Family of I
for b₃ being strict multMagma holds
( b₃ = product F iff ( the carrier of b₃ = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b₃ . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) ) );