theorem Th74: :: GROUP_24:70

for G, A being finite Group
for phi being Homomorphism of A,(AutGroup G) holds card (semidirect_product (G,A,phi)) = (card G) * (card A)