let G be finite cyclic Group; :: thesis: for n, m being Nat st card G = n * m holds

ex a being Element of G st

( ord a = n & gr {a} is strict Subgroup of G )

let n, m be Nat; :: thesis: ( card G = n * m implies ex a being Element of G st

( ord a = n & gr {a} is strict Subgroup of G ) )

consider g being Element of G such that

A1: ord g = card G by GR_CY_1:19;

A2: m in NAT by ORDINAL1:def 12;

A3: n in NAT by ORDINAL1:def 12;

assume card G = n * m ; :: thesis: ex a being Element of G st

( ord a = n & gr {a} is strict Subgroup of G )

then ord (g |^ m) = n by A1, A2, A3, INT_7:30;

then consider a being Element of G such that

A4: ord a = n ;

take a ; :: thesis: ( ord a = n & gr {a} is strict Subgroup of G )

thus ( ord a = n & gr {a} is strict Subgroup of G ) by A4; :: thesis: verum

ex a being Element of G st

( ord a = n & gr {a} is strict Subgroup of G )

let n, m be Nat; :: thesis: ( card G = n * m implies ex a being Element of G st

( ord a = n & gr {a} is strict Subgroup of G ) )

consider g being Element of G such that

A1: ord g = card G by GR_CY_1:19;

A2: m in NAT by ORDINAL1:def 12;

A3: n in NAT by ORDINAL1:def 12;

assume card G = n * m ; :: thesis: ex a being Element of G st

( ord a = n & gr {a} is strict Subgroup of G )

then ord (g |^ m) = n by A1, A2, A3, INT_7:30;

then consider a being Element of G such that

A4: ord a = n ;

take a ; :: thesis: ( ord a = n & gr {a} is strict Subgroup of G )

thus ( ord a = n & gr {a} is strict Subgroup of G ) by A4; :: thesis: verum