for G, H being non empty multMagma
for x being Element of (product <*G,H*>) ex g being Element of G ex h being Element of H st x = <*g,h*>