theorem Th12: :: GROUP_24:26

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x being Element of (semidirect_product (G,A,phi)) ex g being Element of G ex a being Element of A st x = <*g,a*>