theorem Th100: :: GROUP_24:95

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
y * x = (x |^ (n - 1)) * y