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