theorem Th23: :: GROUP_24:32

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for g1, g2 being Element of G
for x, y, z being Element of (semidirect_product (G,A,phi)) st x = <*g1,(1_ A)*> & y = <*g2,(1_ A)*> & z = <*(g1 * g2),(1_ A)*> holds
x * y = z