theorem :: GROUP_4:7

for G being non empty unital associative multMagma
for F being FinSequence of the carrier of G
for a being Element of G holds Product (<*a*> ^ F) = a * (Product F) by FINSOP_1:6;