let G be finite commutative Group; :: thesis:
let m be Nat; :: thesis:
let A be Subset of G; :: thesis:
assume A1: A = { x where x is Element of G : x |^ m = 1_ G } ; :: thesis:
(1_ G) |^ m = 1_ G by GROUP_1:31;
then A2: 1_ G in A by A1;
A3: for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A

let g1, g2 be Element of G; :: thesis:
assume A4: ( g1 in A & g2 in A ) ; :: thesis:
then A5: ex x1 being Element of G st
( g1 = x1 & x1 |^ m = 1_ G ) by A1;
A6: ex x2 being Element of G st
( g2 = x2 & x2 |^ m = 1_ G ) by A1, A4;
(g1 * g2) |^ m = (g1 |^ m) * (g2 |^ m) by GROUP_1:38
.= 1_ G by GROUP_1:def 4, A5, A6 ;
hence g1 * g2 in A by A1; :: thesis:

end;

for g being Element of G st g in A holds
g " in A

let g be Element of G; :: thesis:
assume g in A ; :: thesis:
then A7: ex x being Element of G st
( g = x & x |^ m = 1_ G ) by A1;
(g ") |^ m = (g |^ m) " by GROUP_1:37
.= 1_ G by GROUP_1:8, A7 ;
hence g " in A by A1; :: thesis:

end;

hence ( 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 ) ) by A2, A3; :: thesis: