let G be Group; :: thesis: center G is normal Subgroup of G

now :: thesis: for a being Element of G holds a * (center G) c= (center G) * a

hence
center G is normal Subgroup of G
by GROUP_3:118; :: thesis: verumlet a be Element of G; :: thesis: a * (center G) c= (center G) * a

thus a * (center G) c= (center G) * a :: thesis: verum

end;thus a * (center G) c= (center G) * a :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a * (center G) or x in (center G) * a )

assume x in a * (center G) ; :: thesis: x in (center G) * a

then consider b being Element of G such that

A1: x = a * b and

A2: b in center G by GROUP_2:103;

x = b * a by A1, A2, Th77;

hence x in (center G) * a by A2, GROUP_2:104; :: thesis: verum

end;assume x in a * (center G) ; :: thesis: x in (center G) * a

then consider b being Element of G such that

A1: x = a * b and

A2: b in center G by GROUP_2:103;

x = b * a by A1, A2, Th77;

hence x in (center G) * a by A2, GROUP_2:104; :: thesis: verum