theorem :: GROUP_24:62

for G being Group
for N being strict normal Subgroup of G
for H being Subgroup of G st H,N are_complements_in G holds
for alpha being Homomorphism of H,(AutGroup N) st ( for h, n being Element of G st h in H & n in N holds
for a being Homomorphism of N,N st a = alpha . h holds
a . n = n |^ (h ") ) holds
ex beta being Homomorphism of (semidirect_product (N,H,alpha)),G st
( ( for gh, gn being Element of G
for h being Element of H
for n being Element of N st gh = h & gn = n holds
beta . <*n,h*> = gn * gh ) & beta is bijective )