theorem Th26: :: GROUP_24:35

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