theorem Th38: :: GROUP_24:46

for G, A being Group holds semidirect_product (G,A,(1: (A,(AutGroup G)))) = product <*G,A*>