theorem Th11: :: GROUP_24:25

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x being Element of (semidirect_product (G,A,phi)) holds
( x . 1 in G & x . 2 in A & dom x = {1,2} )