theorem :: GROUP_24:42

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