theorem Th17: :: GROUP_24:29

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds 1_ (semidirect_product (G,A,phi)) = <*(1_ G),(1_ A)*>