theorem Th22: :: GROUP_24:31

for G, A being Group
for phi being Homomorphism of A,(AutGroup G)
for a being Element of A
for g being Element of G
for x being Element of (semidirect_product (G,A,phi)) st x = <*g,a*> holds
x " = <*((phi . (a ")) . (g ")),(a ")*>