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 |^ n = 1_ (Dihedral_group n)
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 |^ n = 1_ (Dihedral_group n)
let x be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> implies x |^ n = 1_ (Dihedral_group n) )
assume A1: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: x |^ n = 1_ (Dihedral_group n)
A2: g1 |^ n = g1 |^ (card (INT.Group n))
.= 1_ (INT.Group n) by GR_CY_1:9 ;
thus x |^ n = <*(g1 |^ n),(1_ (INT.Group 2))*> by A1, Th25
.= <*(1_ (INT.Group n)),(1_ (INT.Group 2))*> by A2
.= 1_ (Dihedral_group n) by Th17 ; :: thesis: verum