:: deftheorem defines Product GROUP_4:def 2 :
for G being non empty multMagma
for F being FinSequence of the carrier of G holds Product F = the multF of G "**" F;