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

proof

thus x |^ 0 = 1_ (semidirect_product (G,A,phi)) by GROUP_1:25
.= <*(1_ G),(1_ A)*> by Th17
.= <*(1_ G),(a |^ 0)*> 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 B1: S₁[i] ; :: thesis: ( S₁[i - 1] & S₁[i + 1] )
B2: x " = <*(1_ G),(a ")*> by A1, Th27;
B3: <*(1_ G),((a |^ i) * (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
.= <*(1_ G),((a |^ i) * (a "))*> by B1, B2, B3, Th26
.= <*(1_ G),((a |^ i) * (a |^ (- 1)))*> by GROUP_1:32
.= <*(1_ G),(a |^ (i + (- 1)))*> by GROUP_1:33
.= <*(1_ G),(a |^ (i - 1))*> ;
hence S₁[i - 1] ; :: thesis: S₁[i + 1]
B4: <*(1_ G),((a |^ i) * a)*> is Element of (semidirect_product (G,A,phi)) by Th9;
x |^ (i + 1) = (x |^ i) * x by GROUP_1:34
.= <*(1_ G),((a |^ i) * a)*> by A1, B1, B4, Th26
.= <*(1_ G),(a |^ (i + 1))*> 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 x |^ i = <*(1_ G),(a |^ i)*> ; :: thesis: verum