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))) = the carrier of (semidirect_product (G,A,phi))
let phi be Homomorphism of A,(AutGroup G); :: thesis: (Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi))) = the carrier of (semidirect_product (G,A,phi))
for x being Element of (semidirect_product (G,A,phi)) holds x in (Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi)))

proof

let x be Element of (semidirect_product (G,A,phi)); :: thesis: x in (Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi)))
consider g being Element of G, a being Element of A such that
B1: ((incl1 (G,A,phi)) . g) * ((incl2 (G,A,phi)) . a) = x by Th32;
( (incl1 (G,A,phi)) . g in Image (incl1 (G,A,phi)) & (incl2 (G,A,phi)) . a in Image (incl2 (G,A,phi)) ) by GROUP_6:45;
hence x in (Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi))) by B1, GROUP_5:4; :: thesis: verum

end;

then the carrier of (semidirect_product (G,A,phi)) c= (Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi))) ;
hence (Image (incl1 (G,A,phi))) * (Image (incl2 (G,A,phi))) = the carrier of (semidirect_product (G,A,phi)) by XBOOLE_0:def 10; :: thesis: verum