:: deftheorem Def1 defines semidirect_product GROUP_24:def 1 :
for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for b₄ being non empty strict multMagma holds
( b₄ = semidirect_product (G,A,phi) iff ( the carrier of b₄ = product (Carrier <*G,A*>) & ( for f, g being Element of product (Carrier <*G,A*>) ex h being Function ex a1 being Element of A ex g2 being Element of G st
( h = the multF of b₄ . (f,g) & a1 = f . 2 & g2 = g . 1 & h . 1 = the multF of G . ((f . 1),((phi . a1) . g2)) & h . 2 = the multF of A . ((f . 2),(g . 2)) ) ) ) );