theorem Th6: :: GROUP_24:18

for G1, G2 being Group
for x being Element of (product <*G1,G2*>) holds
( x . 1 in G1 & x . 2 in G2 & dom x = {1,2} )