theorem Th9: :: GROUP_24:23

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds the carrier of (semidirect_product (G,A,phi)) = the carrier of (product <*G,A*>)