theorem Th16: :: GROUP_24:28

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x, y being Element of (semidirect_product (G,A,phi))
for a being Element of A
for g being Element of G st x = <*g,(1_ A)*> & y = <*(1_ G),a*> holds
x * y = <*g,a*>