let p be natural prime number ; :: thesis: for G being finite strict Group st G is p -group & expon (G,p) = 1 holds
G is cyclic
let G be finite strict Group; :: thesis: ( G is p -group & expon (G,p) = 1 implies G is cyclic )
assume ( G is p -group & expon (G,p) = 1 ) ; :: thesis: G is cyclic
then card G = p |^ 1 by def2
.= p by NEWTON:10 ;
hence G is cyclic by GR_CY_1:45; :: thesis: verum