theorem Th7: :: GROUP_24:19

for G1, G2 being Group
for H1 being Subgroup of G1
for H2 being Subgroup of G2
for h1 being Element of G1 st h1 in H1 holds
for h2 being Element of G2 st h2 in H2 holds
<*h1,h2*> in product <*H1,H2*>