let G be finite Group; :: thesis: for N being normal Subgroup of G st N is Subgroup of center G & G ./. N is cyclic holds
G is commutative
let N be normal Subgroup of G; :: thesis: ( N is Subgroup of center G & G ./. N is cyclic implies G is commutative )
assume that
A1: N is Subgroup of center G and
A2: G ./. N is cyclic ; :: thesis: G is commutative
reconsider I = G ./. N as finite Group ;
consider S being Element of I such that
A3: for T being Element of I ex n being Nat st T = S |^ n by A2, GR_CY_1:18;
consider a1 being Element of G such that
A4: ( S = a1 * N & S = N * a1 ) by GROUP_6:21;
for a, b being Element of G holds a * b = b * a

proof

let a, b be Element of G; :: thesis: a * b = b * a
A5: ( a * N is Element of I & b * N is Element of I ) by GROUP_6:22;
then consider r1 being Nat such that
A6: a * N = S |^ r1 by A3;
a * N = (a1 |^ r1) * N by A4, Th8, A6;
then consider c1 being Element of G such that
A7: ( a = (a1 |^ r1) * c1 & c1 in N ) by Th9;
A8: c1 in center G by A1, A7, GROUP_2:40;
consider r2 being Nat such that
A9: b * N = S |^ r2 by A3, A5;
b * N = (a1 |^ r2) * N by A4, Th8, A9;
then consider c2 being Element of G such that
A10: ( b = (a1 |^ r2) * c2 & c2 in N ) by Th9;
A11: c2 in center G by A1, A10, GROUP_2:40;
a * b = (a1 |^ r1) * (c1 * ((a1 |^ r2) * c2)) by A7, A10, GROUP_1:def 3
.= (a1 |^ r1) * (((a1 |^ r2) * c2) * c1) by A8, GROUP_5:77
.= (a1 |^ r1) * ((a1 |^ r2) * (c2 * c1)) by GROUP_1:def 3
.= ((a1 |^ r1) * (a1 |^ r2)) * (c2 * c1) by GROUP_1:def 3
.= (a1 |^ (r1 + r2)) * (c2 * c1) by GROUP_1:33
.= ((a1 |^ r2) * (a1 |^ r1)) * (c2 * c1) by GROUP_1:33
.= (a1 |^ r2) * ((a1 |^ r1) * (c2 * c1)) by GROUP_1:def 3
.= (a1 |^ r2) * (((a1 |^ r1) * c2) * c1) by GROUP_1:def 3
.= (a1 |^ r2) * ((c2 * (a1 |^ r1)) * c1) by A11, GROUP_5:77
.= (a1 |^ r2) * (c2 * ((a1 |^ r1) * c1)) by GROUP_1:def 3
.= b * a by A7, A10, GROUP_1:def 3 ;
hence a * b = b * a ; :: thesis: verum

end;

hence G is commutative by GROUP_1:def 12; :: thesis: verum