let n be non zero Nat; :: thesis:
let g1 be Element of (INT.Group n); :: thesis:
assume A1: g1 = 1 ; :: thesis:
let a2 be Element of (INT.Group 2); :: thesis:
assume A2: a2 = 1 ; :: thesis:
let x, y, z be Element of (Dihedral_group n); :: thesis:
assume A3: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis:
assume A4: y = <*(1_ (INT.Group n)),a2*> ; :: thesis:
thus ( z in center (Dihedral_group n) implies ( y * z = z * y & ( for i being Nat holds (x |^ i) * z = z * (x |^ i) ) ) ) by GROUP_5:77; :: thesis:
assume A6: y * z = z * y ; :: thesis:
assume A7: for i being Nat holds (x |^ i) * z = z * (x |^ i) ; :: thesis:
for g being Element of (Dihedral_group n) holds z * g = g * z

let g be Element of (Dihedral_group n); :: thesis:
consider k being Nat such that
B1: ( g = (x |^ k) * y or g = x |^ k ) by A1, A2, A3, A4, Th107;

per cases by B1;

suppose B2: g = (x |^ k) * y ; :: thesis:

hence z * g = (z * (x |^ k)) * y by GROUP_1:def 3
.= ((x |^ k) * z) * y by A7
.= (x |^ k) * (z * y) by GROUP_1:def 3
.= (x |^ k) * (y * z) by A6
.= ((x |^ k) * y) * z by GROUP_1:def 3
.= g * z by B2 ;
:: thesis:

end;

suppose B3: g = x |^ k ; :: thesis:

hence z * g = (x |^ k) * z by A7
.= g * z by B3 ;
:: thesis:

end;

end;

end;

hence z in center (Dihedral_group n) by GROUP_5:77; :: thesis: