let p be Element of NAT ; :: thesis: for G being finite strict Group st card G = p & p is prime holds
G is cyclic Group
let G be finite strict Group; :: thesis: ( card G = p & p is prime implies G is cyclic Group )
assume that
A1: card G = p and
A2: p is prime ; :: thesis: G is cyclic Group
ex a being Element of G st ord a = p

proof

assume A3: for a being Element of G holds ord a <> p ; :: thesis: contradiction

A4: now

let a be Element of G; :: thesis: ord a = 1
ord a divides p by A1, Th28;
then ( ord a = 1 or ord a = p ) by A2, INT_2:def 5;
hence ord a = 1 by A3; :: thesis: verum

end;

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

proof

let x be set ; :: 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 A4;
then x9 = 1_ G by GROUP_1:85;
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) by TARSKI:def 3;
then G = (1). G by GROUP_2:70;
then card G = 1 by GROUP_2:81;
hence contradiction by A1, A2, INT_2:def 5; :: thesis: verum

end;

hence G is cyclic Group by A1, Th43; :: thesis: verum