theorem Th108: :: GROUP_24:103

for n being non zero Nat
for g1 being Element of (INT.Group n) st g1 = 1 holds
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 z being Element of (Dihedral_group n) ex k being Nat st
( k < n & ( z = (x |^ k) * y or z = x |^ k ) )