let G be Group; :: thesis: for p being prime Nat holds (1). G is p -group
let p be prime Nat; :: thesis: (1). G is p -group
take 0 ; :: according to GROUP_10:def 17 :: thesis: card ((1). G) = p |^ 0
thus card ((1). G) = 1 by GROUP_2:69
.= p |^ 0 by NEWTON:4 ; :: thesis: verum