theorem :: GROUP_24:39

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds (Image (incl2 (G,A,phi))) /\ (Image (incl1 (G,A,phi))) = (1). (semidirect_product (G,A,phi))