:: deftheorem Def1 defines Product GROUP_17:def 1 :
for G being non empty multMagma
for I being finite set
for b being b₂ -defined the carrier of b₁ -valued total Function
for b₄ being Element of G holds
( b₄ = Product b iff ex f being FinSequence of G st
( b₄ = Product f & f = b * (canFS I) ) );