let G be finite Group; :: thesis: ( G is cyclic iff ex a being Element of G st ord a = card G )
thus ( G is cyclic implies ex a being Element of G st ord a = card G ) :: thesis: ( ex a being Element of G st ord a = card G implies G is cyclic )
proof
reconsider H = multMagma(# the carrier of G, the multF of G #) as Group ;
assume G is cyclic ; :: thesis: ex a being Element of G st ord a = card G
then consider a being Element of G such that
A1: multMagma(# the carrier of G, the multF of G #) = gr {a} ;
take a ; :: thesis: ord a = card G
ord a = card H by A1, Th7;
hence ord a = card G ; :: thesis: verum
end;
given a being Element of G such that A2: ord a = card G ; :: thesis: G is cyclic
ex a being Element of G st multMagma(# the carrier of G, the multF of G #) = gr {a}
proof
consider a being Element of G such that
A3: ord a = card G by A2;
take a ; :: thesis: multMagma(# the carrier of G, the multF of G #) = gr {a}
card (gr {a}) = card G by A3, Th7;
hence multMagma(# the carrier of G, the multF of G #) = gr {a} by GROUP_2:73; :: thesis: verum
end;
hence G is cyclic ; :: thesis: verum