let G be Group; :: thesis: center G is commutative

let a, b be Element of (center G); :: according to GROUP_1:def 12 :: thesis: a * b = b * a

reconsider x = a, y = b as Element of G by GROUP_2:42;

A1: a in center G by STRUCT_0:def 5;

thus a * b = x * y by GROUP_2:43

.= y * x by A1, Th77

.= b * a by GROUP_2:43 ; :: thesis: verum

let a, b be Element of (center G); :: according to GROUP_1:def 12 :: thesis: a * b = b * a

reconsider x = a, y = b as Element of G by GROUP_2:42;

A1: a in center G by STRUCT_0:def 5;

thus a * b = x * y by GROUP_2:43

.= y * x by A1, Th77

.= b * a by GROUP_2:43 ; :: thesis: verum