theorem Th25: :: GROUP_24:34

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