let G, A be Group; :: thesis: 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)*>
let phi be Homomorphism of A,(AutGroup G); :: thesis: 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)*>
let x be Element of (semidirect_product (G,A,phi)); :: thesis: for g being Element of G st x = <*g,(1_ A)*> holds
for i being Integer holds x |^ i = <*(g |^ i),(1_ A)*>
let g be Element of G; :: thesis: ( x = <*g,(1_ A)*> implies for i being Integer holds x |^ i = <*(g |^ i),(1_ A)*> )
assume A1: x = <*g,(1_ A)*> ; :: thesis: for i being Integer holds x |^ i = <*(g |^ i),(1_ A)*>
defpred S₁[ Integer] means x |^ $1 = <*(g |^ $1),(1_ A)*>;
A2: S₁[ 0 ]

proof

thus x |^ 0 = 1_ (semidirect_product (G,A,phi)) by GROUP_1:25
.= <*(1_ G),(1_ A)*> by Th17
.= <*(g |^ 0),(1_ A)*> by GROUP_1:25 ; :: thesis: verum

end;

A3: for i being Integer st S₁[i] holds
( S₁[i - 1] & S₁[i + 1] )

proof

let i be Integer; :: thesis: ( S₁[i] implies ( S₁[i - 1] & S₁[i + 1] ) )
assume S₁[i] ; :: thesis: ( S₁[i - 1] & S₁[i + 1] )
then B1: x |^ i = <*(g |^ i),(1_ A)*> ;
B2: x " = <*(g "),(1_ A)*> by A1, Th24;
B3: <*((g |^ i) * (g ")),(1_ A)*> is Element of (semidirect_product (G,A,phi)) by Th9;
x |^ (i - 1) = x |^ (i + (- 1))
.= (x |^ i) * (x |^ (- 1)) by GROUP_1:33
.= (x |^ i) * (x ") by GROUP_1:32
.= <*((g |^ i) * (g ")),(1_ A)*> by B1, B2, B3, Th23
.= <*((g |^ i) * (g |^ (- 1))),(1_ A)*> by GROUP_1:32
.= <*(g |^ (i + (- 1))),(1_ A)*> by GROUP_1:33
.= <*(g |^ (i - 1)),(1_ A)*> ;
hence S₁[i - 1] ; :: thesis: S₁[i + 1]
B4: <*((g |^ i) * g),(1_ A)*> is Element of (semidirect_product (G,A,phi)) by Th9;
x |^ (i + 1) = (x |^ i) * x by GROUP_1:34
.= <*((g |^ i) * g),(1_ A)*> by A1, B1, B4, Th23
.= <*(g |^ (i + 1)),(1_ A)*> by GROUP_1:34 ;
hence S₁[i + 1] ; :: thesis: verum

end;

for i being Integer holds S₁[i] from INT_1:sch 4(A2, A3);
hence for i being Integer holds x |^ i = <*(g |^ i),(1_ A)*> ; :: thesis: verum