let G be strict Group; :: thesis: for a being Element of G st G is finite & G = gr {a} holds

for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)}

let a be Element of G; :: thesis: ( G is finite & G = gr {a} implies for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)} )

assume that

A1: G is finite and

A2: G = gr {a} ; :: thesis: for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)}

let G1 be strict Subgroup of G; :: thesis: ex p being Element of NAT st G1 = gr {(a |^ p)}

G is cyclic Group by A2, GR_CY_1:def 7;

then G1 is cyclic Group by A1, GR_CY_1:20;

then consider b being Element of G1 such that

A3: G1 = gr {b} by GR_CY_1:def 7;

reconsider b1 = b as Element of G by GROUP_2:42;

consider p being Element of NAT such that

A4: b1 = a |^ p by A1, A2, Th6;

take p ; :: thesis: G1 = gr {(a |^ p)}

thus G1 = gr {(a |^ p)} by A3, A4, Th3; :: thesis: verum

for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)}

let a be Element of G; :: thesis: ( G is finite & G = gr {a} implies for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)} )

assume that

A1: G is finite and

A2: G = gr {a} ; :: thesis: for G1 being strict Subgroup of G ex p being Element of NAT st G1 = gr {(a |^ p)}

let G1 be strict Subgroup of G; :: thesis: ex p being Element of NAT st G1 = gr {(a |^ p)}

G is cyclic Group by A2, GR_CY_1:def 7;

then G1 is cyclic Group by A1, GR_CY_1:20;

then consider b being Element of G1 such that

A3: G1 = gr {b} by GR_CY_1:def 7;

reconsider b1 = b as Element of G by GROUP_2:42;

consider p being Element of NAT such that

A4: b1 = a |^ p by A1, A2, Th6;

take p ; :: thesis: G1 = gr {(a |^ p)}

thus G1 = gr {(a |^ p)} by A3, A4, Th3; :: thesis: verum