let Gc be finite strict cyclic Group; :: thesis: ( ex k being Element of NAT st card Gc = 2 * k implies ex g1 being Element of Gc st
( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds
g1 = g2 ) ) )
set n = card Gc;
given k being Element of NAT such that A1: card Gc = 2 * k ; :: thesis: ex g1 being Element of Gc st
( ord g1 = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds
g1 = g2 ) )
consider g being Element of Gc such that
A2: Gc = gr {g} by GR_CY_1:def 7;
A3: ord g = card Gc by A2, GR_CY_1:7;
take g |^ k ; :: thesis: ( ord (g |^ k) = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds
g |^ k = g2 ) )
A4: (g |^ k) |^ 2 = g |^ (card Gc) by A1, GROUP_1:35
.= 1_ Gc by GR_CY_1:9 ;
A5: k <> 0 by A1;
A6: for p being Nat st (g |^ k) |^ p = 1_ Gc & p <> 0 holds
2 <= p

proof

let p be Nat; :: thesis: ( (g |^ k) |^ p = 1_ Gc & p <> 0 implies 2 <= p )
assume that
A7: (g |^ k) |^ p = 1_ Gc and
A8: ( p <> 0 & 2 > p ) ; :: thesis: contradiction
A9: ( not g is being_of_order_0 & 1_ Gc = g |^ (k * p) ) by A7, GROUP_1:35, GR_CY_1:6;
( card Gc > k * p & k * p <> 0 ) by A1, A5, A8, XCMPLX_1:6, XREAL_1:68;
hence contradiction by A3, A9, GROUP_1:def 11; :: thesis: verum

end;

not g |^ k is being_of_order_0 by GR_CY_1:6;
hence ord (g |^ k) = 2 by A4, A6, GROUP_1:def 11; :: thesis: for g2 being Element of Gc st ord g2 = 2 holds
g |^ k = g2
let g2 be Element of Gc; :: thesis: ( ord g2 = 2 implies g |^ k = g2 )
consider k1 being Element of NAT such that
A10: g2 = g |^ k1 by A2, Th6;
assume that
A11: ord g2 = 2 and
A12: g |^ k <> g2 ; :: thesis: contradiction

now :: thesis: contradiction

A13: not g is being_of_order_0 by GR_CY_1:6;
consider t, t1 being Nat such that
A14: k1 = (k * t) + t1 and
A15: t1 < k by A5, NAT_1:17;
A16: 2 * t1 < card Gc by A1, A15, XREAL_1:68;
t1 <> 0

proof

assume t1 = 0 ; :: thesis: contradiction
then A17: g |^ k1 = g |^ (k * ((2 * (t div 2)) + (t mod 2))) by A14, NAT_D:2
.= g |^ (((k * 2) * (t div 2)) + (k * (t mod 2)))
.= (g |^ ((k * 2) * (t div 2))) * (g |^ (k * (t mod 2))) by GROUP_1:33
.= ((g |^ (k * 2)) |^ (t div 2)) * (g |^ (k * (t mod 2))) by GROUP_1:35
.= ((1_ Gc) |^ (t div 2)) * (g |^ (k * (t mod 2))) by A4, GROUP_1:35
.= (1_ Gc) * (g |^ (k * (t mod 2))) by GROUP_1:31
.= g |^ (k * (t mod 2)) by GROUP_1:def 4 ;

per cases ( t mod 2 = 0 or t mod 2 = 1 ) by NAT_D:12;

suppose t mod 2 = 0 ; :: thesis: contradiction

then g |^ k1 = 1_ Gc by A17, GROUP_1:25;
hence contradiction by A11, A10, GROUP_1:42; :: thesis: verum

end;

suppose t mod 2 = 1 ; :: thesis: contradiction

hence contradiction by A12, A10, A17; :: thesis: verum

end;

end;

end;

then A18: 2 * t1 <> 0 ;
1_ Gc = (g |^ k1) |^ 2 by A11, A10, GROUP_1:41
.= g |^ (((k * t) + t1) * 2) by A14, GROUP_1:35
.= g |^ (((card Gc) * t) + (t1 * 2)) by A1
.= (g |^ ((card Gc) * t)) * (g |^ (t1 * 2)) by GROUP_1:33
.= ((g |^ (ord g)) |^ t) * (g |^ (t1 * 2)) by A3, GROUP_1:35
.= ((1_ Gc) |^ t) * (g |^ (t1 * 2)) by GROUP_1:41
.= (1_ Gc) * (g |^ (t1 * 2)) by GROUP_1:31
.= g |^ (2 * t1) by GROUP_1:def 4 ;
hence contradiction by A3, A18, A16, A13, GROUP_1:def 11; :: thesis: verum

end;

hence contradiction ; :: thesis: verum