let G be Group; :: thesis: for H being Subgroup of G
for N being strict normal Subgroup of G
for phi being Homomorphism of H,(AutGroup N) ex psi being Function of (semidirect_product (N,H,phi)),G st
( ( for n, h being Element of G st n in N & h in H holds
psi . <*n,h*> = n * h ) & ( psi is one-to-one implies N /\ H = (1). G ) & ( N /\ H = (1). G implies psi is one-to-one ) )
let H be Subgroup of G; :: thesis: for N being strict normal Subgroup of G
for phi being Homomorphism of H,(AutGroup N) ex psi being Function of (semidirect_product (N,H,phi)),G st
( ( for n, h being Element of G st n in N & h in H holds
psi . <*n,h*> = n * h ) & ( psi is one-to-one implies N /\ H = (1). G ) & ( N /\ H = (1). G implies psi is one-to-one ) )
let N be strict normal Subgroup of G; :: thesis: for phi being Homomorphism of H,(AutGroup N) ex psi being Function of (semidirect_product (N,H,phi)),G st
( ( for n, h being Element of G st n in N & h in H holds
psi . <*n,h*> = n * h ) & ( psi is one-to-one implies N /\ H = (1). G ) & ( N /\ H = (1). G implies psi is one-to-one ) )
let phi be Homomorphism of H,(AutGroup N); :: thesis: ex psi being Function of (semidirect_product (N,H,phi)),G st
( ( for n, h being Element of G st n in N & h in H holds
psi . <*n,h*> = n * h ) & ( psi is one-to-one implies N /\ H = (1). G ) & ( N /\ H = (1). G implies psi is one-to-one ) )
A1: for f being Function of (product (Carrier <*N,H*>)),G holds f is Function of (semidirect_product (N,H,phi)),G

proof

let f be Function of (product (Carrier <*N,H*>)),G; :: thesis: f is Function of (semidirect_product (N,H,phi)),G
the carrier of (semidirect_product (N,H,phi)) = product (Carrier <*N,H*>) by Def1;
hence f is Function of (semidirect_product (N,H,phi)),G ; :: thesis: verum

end;

consider psi being Function of (product (Carrier <*N,H*>)),G such that
A2: ( ( for n, h being Element of G st n in N & h in H holds
psi . <*n,h*> = n * h ) & ( psi is one-to-one implies N /\ H = (1). G ) & ( N /\ H = (1). G implies psi is one-to-one ) ) by Th59;
reconsider psi = psi as Function of (semidirect_product (N,H,phi)),G by A1;
take psi ; :: thesis: ( ( for n, h being Element of G st n in N & h in H holds
psi . <*n,h*> = n * h ) & ( psi is one-to-one implies N /\ H = (1). G ) & ( N /\ H = (1). G implies psi is one-to-one ) )
thus ( ( for n, h being Element of G st n in N & h in H holds
psi . <*n,h*> = n * h ) & ( psi is one-to-one implies N /\ H = (1). G ) & ( N /\ H = (1). G implies psi is one-to-one ) ) by A2; :: thesis: verum