let G be finite commutative Group; :: thesis: 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 ) )

let m be Nat; :: thesis: 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 ) )

let A be Subset of G; :: thesis: ( A = { x where x is Element of G : x |^ m = 1_ G } implies ( 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 ) ) )

assume A1: A = { x where x is Element of G : x |^ m = 1_ G } ; :: thesis: ( 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 ) )

(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
proof
let g1, g2 be Element of G; :: thesis: ( g1 in A & g2 in A implies g1 * g2 in A )
assume A4: ( g1 in A & g2 in A ) ; :: thesis: g1 * g2 in A
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 ;
hence g1 * g2 in A by A1; :: thesis: verum
end;
for g being Element of G st g in A holds
g " in A
proof
let g be Element of G; :: thesis: ( g in A implies g " in A )
assume g in A ; :: thesis: g " in A
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 ;
hence g " in A by A1; :: thesis: verum
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: verum