let G, A be Group; :: thesis: for phi being Homomorphism of A,(AutGroup G) holds the carrier of (semidirect_product (G,A,phi)) = the carrier of (product <*G,A*>)
let phi be Homomorphism of A,(AutGroup G); :: thesis: the carrier of (semidirect_product (G,A,phi)) = the carrier of (product <*G,A*>)
thus the carrier of (semidirect_product (G,A,phi)) = product (Carrier <*G,A*>) by Def1
.= the carrier of (product <*G,A*>) by GROUP_7:def 2 ; :: thesis: verum