let G be Group; :: thesis: for H being Subgroup of G holds
( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H )
let H be Subgroup of G; :: thesis: ( H is normal Subgroup of G iff for a being Element of G holds H * a c= a * H )
thus ( H is normal Subgroup of G implies for a being Element of G holds H * a c= a * H ) by Th140; :: thesis: ( ( for a being Element of G holds H * a c= a * H ) implies H is normal Subgroup of G )
assume A1: for a being Element of G holds H * a c= a * H ; :: thesis: H is normal Subgroup of G

A2: now

let a be Element of G; :: thesis: a * H c= H * a
H * (a ") c= (a ") * H by A1;
then a * (H * (a ")) c= a * ((a ") * H) by Th4;
then a * (H * (a ")) c= (a * (a ")) * H by GROUP_2:105;
then a * (H * (a ")) c= (1_ G) * H by GROUP_1:def 5;
then a * (H * (a ")) c= carr H by GROUP_2:109;
then (a * H) * (a ") c= carr H by GROUP_2:106;
then ((a * H) * (a ")) * a c= (carr H) * a by Th4;
then (a * H) * ((a ") * a) c= H * a by GROUP_2:34;
then (a * H) * (1_ G) c= H * a by GROUP_1:def 5;
hence a * H c= H * a by GROUP_2:37; :: thesis: verum

end;

now

let a be Element of G; :: thesis: a * H = H * a
( a * H c= H * a & H * a c= a * H ) by A1, A2;
hence a * H = H * a by XBOOLE_0:def 10; :: thesis: verum

end;

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