theorem Th32: :: GROUP_24:40

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x being Element of (semidirect_product (G,A,phi)) ex g being Element of G ex a being Element of A st ((incl1 (G,A,phi)) . g) * ((incl2 (G,A,phi)) . a) = x