theorem Th33: :: GROUP_24:41

for G, A being Group
for phi being Homomorphism of A,(AutGroup G) holds (Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi))) = the carrier of (semidirect_product (G,A,phi))