let n be non zero even Nat; :: thesis: ( n > 2 implies INT.Group 2, center (Dihedral_group n) are_isomorphic )
assume A1: n > 2 ; :: thesis: INT.Group 2, center (Dihedral_group n) are_isomorphic
consider k being Nat such that
A2: n = 2 * k by ABIAN:def 2;
2 < k * 2 by A1, A2;
then 2 * (1 / 2) < (2 * k) * (1 / 2) by XREAL_1:68;
then A3: 1 < k ;
( 1 < 2 & 2 < n ) by A1;
then 1 < n by XXREAL_0:2;
then 1 in Segm n by NAT_1:44;
then 1 in INT.Group n by Th76;
then reconsider g1 = 1 as Element of (INT.Group n) ;
reconsider x = <*g1,(1_ (INT.Group 2))*> as Element of (Dihedral_group n) by Th9;
for z being object holds
( z in the carrier of (center (Dihedral_group n)) iff z in {(1_ (Dihedral_group n)),(x |^ k)} )

proof

let z be object ; :: thesis: ( z in the carrier of (center (Dihedral_group n)) iff z in {(1_ (Dihedral_group n)),(x |^ k)} )
B1: ( g1 = 1 & x = <*g1,(1_ (INT.Group 2))*> ) ;

hereby :: thesis: ( z in {(1_ (Dihedral_group n)),(x |^ k)} implies z in the carrier of (center (Dihedral_group n)) )

assume z in the carrier of (center (Dihedral_group n)) ; :: thesis: z in {(1_ (Dihedral_group n)),(x |^ k)}
then B2: z in center (Dihedral_group n) ;
then z in Dihedral_group n by GROUP_2:40;
then reconsider z1 = z as Element of (Dihedral_group n) ;
z1 in center (Dihedral_group n) by B2;
then ( z1 = 1_ (Dihedral_group n) or z1 = x |^ k ) by A1, A2, Th122;
hence z in {(1_ (Dihedral_group n)),(x |^ k)} by TARSKI:def 2; :: thesis: verum

end;

assume B3: z in {(1_ (Dihedral_group n)),(x |^ k)} ; :: thesis: z in the carrier of (center (Dihedral_group n))
then ( z = 1_ (Dihedral_group n) or z = x |^ k ) by TARSKI:def 2;
then reconsider z1 = z as Element of (Dihedral_group n) ;
( z1 = 1_ (Dihedral_group n) or z1 = x |^ k ) by B3, TARSKI:def 2;
then z1 in center (Dihedral_group n) by A1, A2, B1, Th122;
hence z in the carrier of (center (Dihedral_group n)) ; :: thesis: verum

end;

then ( the carrier of (center (Dihedral_group n)) c= {(1_ (Dihedral_group n)),(x |^ k)} & {(1_ (Dihedral_group n)),(x |^ k)} c= the carrier of (center (Dihedral_group n)) ) ;
then A4: the carrier of (center (Dihedral_group n)) = {(1_ (Dihedral_group n)),(x |^ k)} by XBOOLE_0:def 10;
A5: card (center (Dihedral_group n)) = 2

proof

0 < k by A3;
then k < k + k by XREAL_1:29;
then ( k < n & k <> 0 ) by A2;
then x |^ k <> 1_ (Dihedral_group n) by Th102;
then card {(1_ (Dihedral_group n)),(x |^ k)} = 2 by CARD_2:57;
hence card (center (Dihedral_group n)) = 2 by A4; :: thesis: verum

end;

card (INT.Group 2) = 2 ;
hence INT.Group 2, center (Dihedral_group n) are_isomorphic by A5, GR_CY_2:19; :: thesis: verum