let p be natural prime number ; :: thesis: for G being finite strict Group st card G = p holds
G is p -commutative-group
let G be finite strict Group; :: thesis: ( card G = p implies G is p -commutative-group )
assume A1: card G = p ; :: thesis: G is p -commutative-group
p = p |^ 1 by NEWTON:5;
then A2: G is p -group by A1, GROUP_10:def 17;
G is cyclic Group by A1, GR_CY_1:21;
hence G is p -commutative-group by A2; :: thesis: verum