theorem Th14: :: GROUP_24:27

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for x, y being Element of (semidirect_product (G,A,phi))
for a1, a2 being Element of A
for g1, g2, g3 being Element of G st x = <*g1,a1*> & y = <*g2,a2*> & g3 = (phi . a1) . g2 holds
x * y = <*(g1 * g3),(a1 * a2)*>