let n be non zero Nat; :: thesis: for g1 being Element of (INT.Group n)
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
x " = x |^ (n - 1)
let g1 be Element of (INT.Group n); :: thesis: for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
x " = x |^ (n - 1)
let x be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> implies x " = x |^ (n - 1) )
assume A1: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: x " = x |^ (n - 1)
A2: x * (x |^ (n - 1)) = x |^ (1 + (n - 1)) by GROUP_1:34
.= 1_ (Dihedral_group n) by A1, Th101 ;
(x |^ (n - 1)) * x = x |^ ((n - 1) + 1) by GROUP_1:34
.= 1_ (Dihedral_group n) by A1, Th101 ;
hence x " = x |^ (n - 1) by A2, GROUP_1:5; :: thesis: verum