for H being non empty multMagma
for P, Q being Subset of H holds the multF of H .: [:P,Q:] = P * Q