for G being non empty unital associative multMagma
for F1, F2 being FinSequence of the carrier of G holds Product (F1 ^ F2) = (Product F1) * (Product F2) by FINSOP_1:5;