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

g " in A

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) ) by A2, A3; :: thesis: verum

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

for g being Element of G st g in A holds
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 GROUP_1:def 4, A5, A6 ;

hence g1 * g2 in A by A1; :: thesis: verum

end;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 GROUP_1:def 4, A5, A6 ;

hence g1 * g2 in A by A1; :: thesis: verum

g " in A

proof

hence
( A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
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 GROUP_1:8, A7 ;

hence g " in A by A1; :: thesis: verum

end;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 GROUP_1:8, A7 ;

hence g " in A by A1; :: thesis: verum

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) ) by A2, A3; :: thesis: verum