let n be non zero Nat; :: thesis: for a2 being Element of (INT.Group 2)
for y being Element of (Dihedral_group n) st y = <*(1_ (INT.Group n)),a2*> holds
y * y = 1_ (Dihedral_group n)
let a2 be Element of (INT.Group 2); :: thesis: for y being Element of (Dihedral_group n) st y = <*(1_ (INT.Group n)),a2*> holds
y * y = 1_ (Dihedral_group n)
let y be Element of (Dihedral_group n); :: thesis: ( y = <*(1_ (INT.Group n)),a2*> implies y * y = 1_ (Dihedral_group n) )
assume A1: y = <*(1_ (INT.Group n)),a2*> ; :: thesis: y * y = 1_ (Dihedral_group n)
A2: a2 |^ 2 = a2 |^ (card (INT.Group 2))
.= 1_ (INT.Group 2) by GR_CY_1:9 ;
thus y * y = y |^ 2 by GROUP_1:27
.= <*(1_ (INT.Group n)),(a2 |^ 2)*> by A1, Th28
.= <*(1_ (INT.Group n)),(1_ (INT.Group 2))*> by A2
.= 1_ (Dihedral_group n) by Th17 ; :: thesis: verum