for L being non empty unital associative commutative multMagma
for f, g being FinSequence of L
for p being Permutation of (dom f) st g = f * p holds
Product g = Product f