theorem :: GROUP_24:24

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G holds <*g,a*> is Element of (semidirect_product (G,A,phi)) by Th9;