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

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

A3: now :: thesis:

let a be Element of G; :: thesis:
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:

end;

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

let x be object ; :: thesis:
assume x in the carrier of G ; :: thesis:
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:

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:

end;

hence G is cyclic by Th19; :: thesis: