let G be finite Group; :: thesis: for N being normal Subgroup of G st N = center G & G ./. N is cyclic holds
G is commutative
let N be normal Subgroup of G; :: thesis: ( N = center G & G ./. N is cyclic implies G is commutative )
assume A1: ( N = center G & G ./. N is cyclic ) ; :: thesis: G is commutative
then N is Subgroup of center G by GROUP_2:54;
hence G is commutative by A1, Th10; :: thesis: verum