theorem Th1: :: TOPALG_4:1

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*>