theorem Th28: :: GROUP_24:37

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