let G be finite strict Group; :: thesis: ( card G is prime implies G is cyclic )
assume A1: card G is prime ; :: thesis: G is cyclic
set p = card G;
ex a being Element of G st ord a = card G

proof

assume A2: for a being Element of G holds ord a <> card G ; :: thesis: contradiction

A3: now :: thesis: for a being Element of G holds ord a = 1

let a be Element of G; :: thesis: ord a = 1
ord a divides card G by Th8;
then ( ord a = 1 or ord a = card G ) by A1, INT_2:def 4;
hence ord a = 1 by A2; :: thesis: verum

end;

for x being object st x in the carrier of G holds
x in the carrier of ((1). G)

proof

let x be object ; :: thesis: ( x in the carrier of G implies x in the carrier of ((1). G) )
assume x in the carrier of G ; :: thesis: x in the carrier of ((1). G)
then reconsider x9 = x as Element of G ;
ord x9 = 1 by A3;
then x9 = 1_ G by GROUP_1:43;
then x9 in {(1_ G)} by TARSKI:def 1;
hence x in the carrier of ((1). G) by GROUP_2:def 7; :: thesis: verum

end;

then the carrier of G c= the carrier of ((1). G) ;
then G = (1). G by GROUP_2:61;
then card G = 1 by GROUP_2:69;
hence contradiction by A1, INT_2:def 4; :: thesis: verum

end;

hence G is cyclic by Th19; :: thesis: verum