let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G) holds (Image (incl1 (G,A,phi))) "\/" (Image (incl2 (G,A,phi))) = semidirect_product (G,A,phi)
let phi be Homomorphism of A,(AutGroup G); :: thesis: (Image (incl1 (G,A,phi))) "\/" (Image (incl2 (G,A,phi))) = semidirect_product (G,A,phi)
set S = semidirect_product (G,A,phi);
set U = (Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi)));
(Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi))) c= the carrier of (gr ((Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi))))) by GROUP_4:def 4;
then the carrier of (semidirect_product (G,A,phi)) c= the carrier of (gr ((Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi))))) by Th33;
then semidirect_product (G,A,phi) = gr ((Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi)))) by GROUP_2:61;
hence (Image (incl1 (G,A,phi))) "\/" (Image (incl2 (G,A,phi))) = semidirect_product (G,A,phi) by GROUP_4:50; :: thesis: verum