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

ex H being finite strict Subgroup of G st

( the carrier of H = A & H is commutative & H is normal )

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

ex H being finite strict Subgroup of G st

( the carrier of H = A & H is commutative & H is normal )

let A be Subset of G; :: thesis: ( A = { x where x is Element of G : x |^ m = 1_ G } implies ex H being finite strict Subgroup of G st

( the carrier of H = A & H is commutative & H is normal ) )

assume A = { x where x is Element of G : x |^ m = 1_ G } ; :: thesis: ex H being finite strict Subgroup of G st

( the carrier of H = A & H is commutative & H is normal )

then ( 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 Th13;

then consider H being strict Subgroup of G such that

A1: the carrier of H = A by GROUP_2:52;

H is normal by GROUP_3:116;

hence ex H being finite strict Subgroup of G st

( the carrier of H = A & H is commutative & H is normal ) by A1; :: thesis: verum

for A being Subset of G st A = { x where x is Element of G : x |^ m = 1_ G } holds

ex H being finite strict Subgroup of G st

( the carrier of H = A & H is commutative & H is normal )

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

ex H being finite strict Subgroup of G st

( the carrier of H = A & H is commutative & H is normal )

let A be Subset of G; :: thesis: ( A = { x where x is Element of G : x |^ m = 1_ G } implies ex H being finite strict Subgroup of G st

( the carrier of H = A & H is commutative & H is normal ) )

assume A = { x where x is Element of G : x |^ m = 1_ G } ; :: thesis: ex H being finite strict Subgroup of G st

( the carrier of H = A & H is commutative & H is normal )

then ( 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 Th13;

then consider H being strict Subgroup of G such that

A1: the carrier of H = A by GROUP_2:52;

H is normal by GROUP_3:116;

hence ex H being finite strict Subgroup of G st

( the carrier of H = A & H is commutative & H is normal ) by A1; :: thesis: verum