let G, A be finite Group; :: thesis: for phi being Homomorphism of A,(AutGroup G) holds card (semidirect_product (G,A,phi)) = (card G) * (card A)
let phi be Homomorphism of A,(AutGroup G); :: thesis: card (semidirect_product (G,A,phi)) = (card G) * (card A)
set UG = the carrier of G;
set UA = the carrier of A;
A1: Carrier <*G,A*> = <* the carrier of G, the carrier of A*> by PRALG_1:18;
card (semidirect_product (G,A,phi)) = card (product (Carrier <*G,A*>)) by Def1
.= card (product <* the carrier of G, the carrier of A*>) by A1
.= (card the carrier of G) * (card the carrier of A) by GROUP_17:2 ;
hence card (semidirect_product (G,A,phi)) = (card G) * (card A) ; :: thesis: verum