theorem :: GROUP_24:99

for n being non zero Nat
for g1 being Element of (INT.Group n)
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for j being Nat holds (x |^ j) " = x |^ (n - j)