theorem Th109: :: GROUP_24:104

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