theorem Th13: :: GROUP_17:13

for G being finite commutative Group
for m being Nat
for A being Subset of G st A = { x where x is Element of G : x |^ m = 1_ G } holds
( A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) )