theorem Th20: :: GROUP_24:30

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,a*> & y = <*((phi . (a ")) . (g ")),(a ")*> holds
( x * y = 1_ (semidirect_product (G,A,phi)) & y * x = 1_ (semidirect_product (G,A,phi)) )