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 9;
take g |^ k ; :: thesis: ( ord (g |^ k) = 2 & ( for g2 being Element of Gc st ord g2 = 2 holds
g |^ k = g2 ) )
A3: (g |^ k) |^ 2 = g |^ (card Gc) by A1, GROUP_1:67
.= 1_ Gc by GR_CY_1:29 ;
A4: not g |^ k is being_of_order_0 by GR_CY_1:26;
A5: ord g = card Gc by A2, GR_CY_1:27;
A6: ( k <> 0 & 2 <> 0 ) by A1, GROUP_1:90;
then A7: k > 0 ;
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
A8: (g |^ k) |^ p = 1_ Gc and
A9: p <> 0 and
A10: 2 > p ; :: thesis: contradiction
A11: card Gc > k * p by A1, A7, A10, XREAL_1:70;
A12: not g is being_of_order_0 by GR_CY_1:26;
A13: k * p <> 0 by A6, A9, XCMPLX_1:6;
1_ Gc = g |^ (k * p) by A8, GROUP_1:67;
hence contradiction by A5, A11, A12, A13, GROUP_1:def 12; :: thesis: verum

end;

hence ord (g |^ k) = 2 by A3, A4, GROUP_1:def 12; :: 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 )
assume that
A14: ord g2 = 2 and
A15: g |^ k <> g2 ; :: thesis: contradiction
consider k1 being Element of NAT such that
A16: g2 = g |^ k1 by A2, Th12;

now

consider t, t1 being Nat such that
A17: k1 = (k * t) + t1 and
A18: t1 < k by A7, NAT_1:17;
t1 <> 0

proof

assume t1 = 0 ; :: thesis: contradiction
then A19: g |^ k1 = g |^ (k * ((2 * (t div 2)) + (t mod 2))) by A17, 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:63
.= ((g |^ (k * 2)) |^ (t div 2)) * (g |^ (k * (t mod 2))) by GROUP_1:67
.= ((1_ Gc) |^ (t div 2)) * (g |^ (k * (t mod 2))) by A3, GROUP_1:67
.= (1_ Gc) * (g |^ (k * (t mod 2))) by GROUP_1:61
.= g |^ (k * (t mod 2)) by GROUP_1:def 5 ;

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 A19, GROUP_1:43;
hence contradiction by A14, A16, GROUP_1:84; :: thesis: verum

end;

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

hence contradiction by A15, A16, A19; :: thesis: verum

end;

end;

end;

then A20: 2 * t1 <> 0 ;
A21: 2 * t1 < card Gc by A1, A18, XREAL_1:70;
A22: g |^ (2 * t1) = 1_ Gc

proof

thus 1_ Gc = (g |^ k1) |^ 2 by A14, A16, GROUP_1:82
.= g |^ (((k * t) + t1) * 2) by A17, GROUP_1:67
.= g |^ (((card Gc) * t) + (t1 * 2)) by A1
.= (g |^ ((card Gc) * t)) * (g |^ (t1 * 2)) by GROUP_1:63
.= ((g |^ (ord g)) |^ t) * (g |^ (t1 * 2)) by A5, GROUP_1:67
.= ((1_ Gc) |^ t) * (g |^ (t1 * 2)) by GROUP_1:82
.= (1_ Gc) * (g |^ (t1 * 2)) by GROUP_1:61
.= g |^ (2 * t1) by GROUP_1:def 5 ; :: thesis: verum

end;

not g is being_of_order_0 by GR_CY_1:26;
hence contradiction by A5, A20, A21, A22, GROUP_1:def 12; :: thesis: verum

end;

hence contradiction ; :: thesis: verum