let G be Group; :: thesis: for H being Subgroup of G st H is Subgroup of center G holds
H is normal Subgroup of G
let H be Subgroup of G; :: thesis: ( H is Subgroup of center G implies H is normal Subgroup of G )
assume A1: H is Subgroup of center G ; :: thesis: H is normal Subgroup of G

now :: thesis: for a being Element of G holds H * a c= a * H

let a be Element of G; :: thesis: H * a c= a * H
thus H * a c= a * H :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H * a or x in a * H )
assume x in H * a ; :: thesis: x in a * H
then consider b being Element of G such that
A2: x = b * a and
A3: b in H by GROUP_2:104;
b in center G by A1, A3, GROUP_2:40;
then x = a * b by A2, Th77;
hence x in a * H by A3, GROUP_2:103; :: thesis: verum

end;

end;

hence H is normal Subgroup of G by GROUP_3:119; :: thesis: verum