theorem Th27: :: GROUP_24:36

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