let n be Element of NAT ; :: thesis: for G being finite strict Group st G is cyclic & card G = n holds
for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
let G be finite strict Group; :: thesis: ( G is cyclic & card G = n implies for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) ) )
assume that
A1: G is cyclic and
A2: card G = n ; :: thesis: for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
let p be Element of NAT ; :: thesis: ( p divides n implies ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) ) )
assume A3: p divides n ; :: thesis: ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )

proof

consider s being Nat such that
A4: n = p * s by A3, NAT_D:def 3;
consider a being Element of G such that
A5: G = gr {a} by A1;
take gr {(a |^ s)} ; :: thesis: ( card (gr {(a |^ s)}) = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = gr {(a |^ s)} ) )
A6: s in NAT by ORDINAL1:def 12;
then A7: ord (a |^ s) = p by A2, A5, A4, Th8;
then A8: card (gr {(a |^ s)}) = p by GR_CY_1:7;
for G2 being strict Subgroup of G st card G2 = p holds
G2 = gr {(a |^ s)}

proof

let G2 be strict Subgroup of G; :: thesis: ( card G2 = p implies G2 = gr {(a |^ s)} )
assume A9: card G2 = p ; :: thesis: G2 = gr {(a |^ s)}
consider k being Element of NAT such that
A10: G2 = gr {(a |^ k)} by A5, Th7;
n divides k * p by A2, A5, A9, A10, Th11;
then consider m being Nat such that
A11: k * p = n * m by NAT_D:def 3;
ex l being Nat st k = s * l

proof

take m ; :: thesis: k = s * m
reconsider p1 = p as Integer ;
A12: p <> 0 by A2, A4;
((1 / p1) * p1) * k = (1 / p1) * ((p1 * s) * m) by A4, A11, XCMPLX_1:4;
then 1 * k = ((p1 * (1 / p1)) * s) * m by A12, XCMPLX_1:106;
then k = (1 * s) * m by A12, XCMPLX_1:106;
hence k = s * m ; :: thesis: verum

end;

then s divides k by NAT_D:def 3;
hence G2 = gr {(a |^ s)} by A6, A8, A9, A10, Th9, Th10; :: thesis: verum

end;

hence ( card (gr {(a |^ s)}) = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = gr {(a |^ s)} ) ) by A7, GR_CY_1:7; :: thesis: verum

end;

hence ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) ) ; :: thesis: verum